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 φ ψ ψ φ


Step Hyp Ref Expression
1 bicom1 φ ψ ψ φ
2 bicom1 ψ φ φ ψ
3 1 2 impbii φ ψ ψ φ