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

Metamath Proof Explorer

Theorem pm5.501

Description: Theorem *5.501 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm5.501 ⊢ φ → ψ ↔ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 pm5.1im ⊢ φ → ψ → φ ↔ ψ
2 biimp ⊢ φ ↔ ψ → φ → ψ
3 2 com12 ⊢ φ → φ ↔ ψ → ψ
4 1 3 impbid ⊢ φ → ψ ↔ φ ↔ ψ