Theorem 3impexpbicom 1287

Description: 3impexp 1286 with biconditional consequent of antecedent that is commuted in consequent. Derived automatically from 3impexpVD 16680. (Contributed by Alan Sare, 31-Dec-2011.)

Assertion

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

Proof of Theorem 3impexpbicom

Step	Hyp	Ref	Expression
1		bicom 579	. . . 4 |- ((th <-> ta) <-> (ta <-> th))
2		imbi2 686	. . . . 5 |- (((th <-> ta) <-> (ta <-> th)) -> (((ph /\ ps /\ ch) -> (th <-> ta)) <-> ((ph /\ ps /\ ch) -> (ta <-> th))))
3	2	biimpcd 172	. . . 4 |- (((ph /\ ps /\ ch) -> (th <-> ta)) -> (((th <-> ta) <-> (ta <-> th)) -> ((ph /\ ps /\ ch) -> (ta <-> th))))
4	1, 3	mpi 55	. . 3 |- (((ph /\ ps /\ ch) -> (th <-> ta)) -> ((ph /\ ps /\ ch) -> (ta <-> th)))
5	4	3expd 1085	. 2 |- (((ph /\ ps /\ ch) -> (th <-> ta)) -> (ph -> (ps -> (ch -> (ta <-> th)))))
6		3impexp 1286	. . . 4 |- (((ph /\ ps /\ ch) -> (ta <-> th)) <-> (ph -> (ps -> (ch -> (ta <-> th)))))
7	6	biimpri 169	. . 3 |- ((ph -> (ps -> (ch -> (ta <-> th)))) -> ((ph /\ ps /\ ch) -> (ta <-> th)))
8	7, 1	syl6ibr 230	. 2 |- ((ph -> (ps -> (ch -> (ta <-> th)))) -> ((ph /\ ps /\ ch) -> (th <-> ta)))
9	5, 8	impbii 174	1 |- (((ph /\ ps /\ ch) -> (th <-> ta)) <-> (ph -> (ps -> (ch -> (ta <-> th)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ w3a 858

This theorem is referenced by:  3impexpbicomi 1288  3impexpbicomiVD 16682

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain