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

Metamath Proof Explorer

Definition df-3or

Description: Define disjunction ('or') of three wff's. Definition *2.33 of WhiteheadRussell p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass . (Contributed by NM, 8-Apr-1994)

Ref Expression
Assertion df-3or ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wff φ
1 wps wff ψ
2 wch wff χ
3 0 1 2 w3o wff φ ∨ ψ ∨ χ
4 0 1 wo wff φ ∨ ψ
5 4 2 wo wff φ ∨ ψ ∨ χ
6 3 5 wb wff φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ