To see this better, let's look at a couple of interesting direct derivations.
~P |- P->Q
1. ~P
Ass
2. ~PvQ 1 v int
3. P->Q 2 MI
Q |- P->Q
1. Q
Ass
2. ~PvQ 1 v int
3. P->Q 2 MI
A hypothetical or conditional derivation begins with an antecedent assumed or shown to be true. If we can then show an intended consequent is true we are entitled to say that the implication holds. This lets us do many derivations for which we could not use a direct method (and although we could always do an indirect derivation, too often it would be very tedious).
P->Q, Q->R |- P->R
1. P->Q
Ass
2. Q->R
Ass
3. P
Hyp again we indent for a subordinate derivation
4. Q
1,3 -> elim
5. R
2,4 -> elim
6. P->R
3-5 hyp elim
Notice how this is like what we did for indirect derivations with setting up a hypothesis for a subordinate derivation, then eliminating (or discharging) that hypothesis later on.
Ax(Fx -> Gx), Ax(Gx -> Hx) |- Ax(Fx -> Hx)
1. Ax(Fx -> Gx)
Ass
2. Ax(Gx -> Hx)
Ass
3. Fa
Hyp
4. Fa
-> Ga
1 UQ elim
5. Ga
3,4 -> elim
6. Ga
-> Ha
2 UQ elim
7. Ha
5,6 -> elim
8. Fa -> Ha
3-7 hyp elim
9. Ax(Fx -> Hx)
8 UQ int
This last step demands some further explanation.
Ordinarily we could not introduce a universal quantifier with just an assumed
name, but the restriction disappears when we have discharged the hypothesis,
as we do in line 8. The reasoning is that in place of the "a" we
could have used any name at all and had the same results, so we can then
generalize. Compare the problem above with the following invalid
argument form: ~Fa |- Ax(Fx -> Gx).
We could have shown Fa -> Ga, but the name
"a" remains an assumption from the premises, so we could not legitimately
go to the next step and say Ax(Fx -> Gx).
Ax(Fx -> Gb) |- Ex(Fx) -> Gb
Ex(Fx -> Gb) |- Ax(Fx) -> Gb
Note: be very careful not to go against our
"new name" rule.