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

Metamath Proof Explorer

Theorem pm2.31

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

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

Proof

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