Metamath Proof Explorer

Theorem bicom

Description: Commutative law for the biconditional. Theorem *4.21 of WhiteheadRussell p. 117. (Contributed by NM, 11-May-1993)

Ref Expression
Assertion bicom 
|- ( ( ph <-> ps ) <-> ( ps <-> ph ) )

Proof

Step Hyp Ref Expression
1 bicom1 
 |-  ( ( ph <-> ps ) -> ( ps <-> ph ) )
2 bicom1 
 |-  ( ( ps <-> ph ) -> ( ph <-> ps ) )
3 1 2 impbii 
 |-  ( ( ph <-> ps ) <-> ( ps <-> ph ) )