Metamath Proof Explorer


Theorem biimpexp

Description: A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010)

Ref Expression
Assertion biimpexp
|- ( ( ( ph <-> ps ) -> ch ) <-> ( ( ph -> ps ) -> ( ( ps -> ph ) -> ch ) ) )

Proof

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