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

Metamath Proof Explorer

Theorem pm5.63

Description: Theorem *5.63 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 25-Dec-2012)

Ref Expression
Assertion pm5.63 ⊢ φ ∨ ψ ↔ φ ∨ ¬ φ ∧ ψ

Proof

Step Hyp Ref Expression
1 exmid ⊢ φ ∨ ¬ φ
2 ordi ⊢ φ ∨ ¬ φ ∧ ψ ↔ φ ∨ ¬ φ ∧ φ ∨ ψ
3 1 2 mpbiran ⊢ φ ∨ ¬ φ ∧ ψ ↔ φ ∨ ψ
4 3 bicomi ⊢ φ ∨ ψ ↔ φ ∨ ¬ φ ∧ ψ