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

Metamath Proof Explorer

Theorem pm2.32

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

Ref Expression
Assertion pm2.32 ⊢ φ ∨ ψ ∨ χ → φ ∨ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 orass ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ
2 1 biimpi ⊢ φ ∨ ψ ∨ χ → φ ∨ ψ ∨ χ