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

Metamath Proof Explorer

Theorem bicom1

Description: Commutative law for the biconditional. (Contributed by Wolf Lammen, 10-Nov-2012)

Ref Expression
Assertion bicom1 ⊢ φ ↔ ψ → ψ ↔ φ

Proof

Step Hyp Ref Expression
1 biimpr ⊢ φ ↔ ψ → ψ → φ
2 biimp ⊢ φ ↔ ψ → φ → ψ
3 1 2 impbid ⊢ φ ↔ ψ → ψ ↔ φ