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 syl6ibr
 |-  ( ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) -> ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) )
9 5 8 impbii
 |-  ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) <-> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) )