I'm reading Introduction to Mathematical Logic gy by Vilnis Detlovs and Karlis Podnieks, and I'm confused about proofs. In the book, it says that to prove directly you should find ways to substitute the hypoethesis formula(s) into one of the axiom schemas so that other formulas will be implied, with the goal of ultimately leading to the conclusion which one wishes to prove. However, I'm a bit unsure about what types of substitutions are allowed. For instance, take the following axiom schema, "L2": A -> (B -> C) -> (A -> B) -> (A -> C) Can I substitute the same letter in a hypoethesis formula for more than one letter in the schema? For instance: Hypothesis: A -> (A -> C) Conclusion: (A -> A) -> (A -> C) (L2) Where the A from the hypothesis is substituted for A and B (consistently) in the axiom schema. Is this "valid" (to use the word imprecisely)? Thanks.