Originally Posted by

**ToaTerra** To simply things, lets define T as the first-order theory (or propositional logic) and A and can show T+A |- B. I want to show T |- A -> B.

2. For each step S in the deduction which is a premise in Γ (a reiteration step) or an axiom, we can apply modus ponens to the axiom 1, S→(H→S), to get H→S.

This step seems informative. Since A is not a theorem of T it doesn't seem to apply. But suppose there was some formula S such that T |- S, then we would have S -> ((A -> B) -> S) => ((A -> B) -> S)