This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 bicom1 ⊢ φ ↔ ψ → ψ ↔ φ
2 bicom1 ⊢ ψ ↔ φ → φ ↔ ψ
3 1 2 impbii ⊢ φ ↔ ψ ↔ ψ ↔ φ