Metamath Proof Explorer

Theorem aibandbiaiaiffb

Description: A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016)

Ref Expression
Assertion aibandbiaiaiffb 
|- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 dfbi2 
 |-  ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
2 1 biimpri 
 |-  ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) )