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

Metamath Proof Explorer

Theorem pm4.43

Description: Theorem *4.43 of WhiteheadRussell p. 119. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 26-Nov-2012)

Ref Expression
Assertion pm4.43 ⊢ φ ↔ φ ∨ ψ ∧ φ ∨ ¬ ψ

Proof

Step Hyp Ref Expression
1 pm3.24 ⊢ ¬ ψ ∧ ¬ ψ
2 1 biorfri ⊢ φ ↔ φ ∨ ψ ∧ ¬ ψ
3 ordi ⊢ φ ∨ ψ ∧ ¬ ψ ↔ φ ∨ ψ ∧ φ ∨ ¬ ψ
4 2 3 bitri ⊢ φ ↔ φ ∨ ψ ∧ φ ∨ ¬ ψ