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

Metamath Proof Explorer

Theorem pm5.55

Description: Theorem *5.55 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 20-Jan-2013)

Ref Expression
Assertion pm5.55 ⊢ φ ∨ ψ ↔ φ ∨ φ ∨ ψ ↔ ψ

Proof

Step Hyp Ref Expression
1 biort ⊢ φ → φ ↔ φ ∨ ψ
2 1 bicomd ⊢ φ → φ ∨ ψ ↔ φ
3 biorf ⊢ ¬ φ → ψ ↔ φ ∨ ψ
4 3 bicomd ⊢ ¬ φ → φ ∨ ψ ↔ ψ
5 2 4 nsyl5 ⊢ ¬ φ ∨ ψ ↔ φ → φ ∨ ψ ↔ ψ
6 5 orri ⊢ φ ∨ ψ ↔ φ ∨ φ ∨ ψ ↔ ψ