df-3or - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-3or 774

Description: Define disjunction ('or') of 3 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 260.

**Assertion**
Ref	Expression
df-3or	$\/$ $\/$ $\/$ $\/$

**Detailed syntax breakdown of Definition df-3or**
Step	Hyp	Ref	Expression
1		wph	. . 3
2		wps	. . 3
3		wch	. . 3
4	1, 2, 3	w3o 772	. 2 $\/$ $\/$
5	1, 2	wo 222	. . 3 $\/$
6	5, 3	wo 222	. 2 $\/$ $\/$
7	4, 6	wb 146	1 $\/$ $\/$ $\/$ $\/$

Colors of variables: wff set class

This definition is referenced by: 3orass 776 3orrot 779 3orbi123i 821 3ori 882 3jao 883 3orbi123d 889 3orim123d 898 hb3or 1008 eueq3 1910 sspsstri 2138 eltp 2429 wereu 2935 ordtri3or 2969 ordtri1 2970 ordtri3 2973 ordeleqon 2980 onzsl 3107 dflim3 3108 entri 4811 entri2 4812 psslinpr 5107 lttri4t 5487 xrsupss 6025 xrinfmss 6026 nnnegz 6085 elznn0nn 6095 elnnz1 6102