Metamath Proof Explorer


Theorem expcomdg

Description: Biconditional form of expcomd . (Contributed by Alan Sare, 22-Jul-2012) (New usage is discouraged.)

Ref Expression
Assertion expcomdg
|- ( ( ph -> ( ( ps /\ ch ) -> th ) ) <-> ( ph -> ( ch -> ( ps -> th ) ) ) )

Proof

Step Hyp Ref Expression
1 ancomst
 |-  ( ( ( ps /\ ch ) -> th ) <-> ( ( ch /\ ps ) -> th ) )
2 impexp
 |-  ( ( ( ch /\ ps ) -> th ) <-> ( ch -> ( ps -> th ) ) )
3 1 2 bitri
 |-  ( ( ( ps /\ ch ) -> th ) <-> ( ch -> ( ps -> th ) ) )
4 3 imbi2i
 |-  ( ( ph -> ( ( ps /\ ch ) -> th ) ) <-> ( ph -> ( ch -> ( ps -> th ) ) ) )