Theorem 3impexpbicom 1367

Description: 3impexp 1366 with biconditional consequent of antecedent that is commuted in consequent. Derived automatically from 3impexpVD in set.mm. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping.

Assertion

Ref	Expression
3impexpbicom	|- (((ph /\ ps /\ ch) -> (th <-> ta)) <-> (ph -> (ps -> (ch -> (ta <-> th)))))

Proof of Theorem 3impexpbicom

Step	Hyp	Ref	Expression
1		bicom 191	. . . 4 |- ((th <-> ta) <-> (ta <-> th))
2		imbi2 314	. . . . 5 |- (((th <-> ta) <-> (ta <-> th)) -> (((ph /\ ps /\ ch) -> (th <-> ta)) <-> ((ph /\ ps /\ ch) -> (ta <-> th))))
3	2	biimpcd 215	. . . 4 |- (((ph /\ ps /\ ch) -> (th <-> ta)) -> (((th <-> ta) <-> (ta <-> th)) -> ((ph /\ ps /\ ch) -> (ta <-> th))))
4	1, 3	mpi 16	. . 3 |- (((ph /\ ps /\ ch) -> (th <-> ta)) -> ((ph /\ ps /\ ch) -> (ta <-> th)))
5	4	3expd 1168	. 2 |- (((ph /\ ps /\ ch) -> (th <-> ta)) -> (ph -> (ps -> (ch -> (ta <-> th)))))
6		3impexp 1366	. . . 4 |- (((ph /\ ps /\ ch) -> (ta <-> th)) <-> (ph -> (ps -> (ch -> (ta <-> th)))))
7	6	biimpri 197	. . 3 |- ((ph -> (ps -> (ch -> (ta <-> th)))) -> ((ph /\ ps /\ ch) -> (ta <-> th)))
8	7, 1	syl6ibr 218	. 2 |- ((ph -> (ps -> (ch -> (ta <-> th)))) -> ((ph /\ ps /\ ch) -> (th <-> ta)))
9	5, 8	impbii 180	1 |- (((ph /\ ps /\ ch) -> (th <-> ta)) <-> (ph -> (ps -> (ch -> (ta <-> th)))))

Syntax hints:   -> wi 4   <-> wb 176   /\ w3a 934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936

This theorem is referenced by: (None)