Metamath Proof Explorer

Theorem 3impexpbicom

Description: Version of 3impexp where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011)

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

Proof

Step Hyp Ref Expression
1 bicom 
 |-  ( ( th <-> ta ) <-> ( ta <-> th ) )
2 imbi2 
 |-  ( ( ( th <-> ta ) <-> ( ta <-> th ) ) -> ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) <-> ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) ) )
3 2 biimpcd 
 |-  ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) -> ( ( ( th <-> ta ) <-> ( ta <-> th ) ) -> ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) ) )
4 1 3 mpi 
 |-  ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) -> ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) )
5 4 3expd 
 |-  ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) -> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) )
6 3impexp 
 |-  ( ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) <-> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) )
7 6 biimpri 
 |-  ( ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) -> ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) )
8 7 1 imbitrrdi 
 |-  ( ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) -> ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) )
9 5 8 impbii 
 |-  ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) <-> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) )