I'm struggling to see how to derive the deduction theorem from some particular axioms. Basically I've got:
(1) A -> (B -> A)
(2) A -> (B -> C) ->((A -> B) -> (A -> C))
(3) (~A -> ~B) -> (B -> A)
(4) (x)A -> A(t) where t is free for x.
Rules of inference are:
(2*) From A -> B, infer A -> (x)B so long as x does not occur free in A or any premise.
Supposing we are proving the theorem for A, at the inductive step I get stuck showing that if C is derived from D by means of (2*) and we have A -> D, then we have A ->C.
Any help would be really great.