Theorem impexp ≪ | index | src | ≫ 

theorem impexp (a b c: wff): $ a /\ b -> c <-> a -> b -> c $;
StepHypRefExpression
1 anim1 
((a /\ b -> c) /\ a -> a) -> (a /\ b -> c) /\ a /\ b -> a /\ b
2 anr 
(a /\ b -> c) /\ a -> a
3 1, 2 ax_mp 
(a /\ b -> c) /\ a /\ b -> a /\ b
4 anll 
(a /\ b -> c) /\ a /\ b -> a /\ b -> c
5 3, 4 mpd 
(a /\ b -> c) /\ a /\ b -> c
6 5 exp 
(a /\ b -> c) /\ a -> b -> c
7 6 exp 
(a /\ b -> c) -> a -> b -> c
8 anrr 
(a -> b -> c) /\ (a /\ b) -> b
9 anrl 
(a -> b -> c) /\ (a /\ b) -> a
10 anl 
(a -> b -> c) /\ (a /\ b) -> a -> b -> c
11 9, 10 mpd 
(a -> b -> c) /\ (a /\ b) -> b -> c
12 8, 11 mpd 
(a -> b -> c) /\ (a /\ b) -> c
13 12 exp 
(a -> b -> c) -> a /\ b -> c
14 7, 13 ibii 
a /\ b -> c <-> a -> b -> c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)