Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-3or | Structured version Visualization version GIF version |
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 545. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
df-3or | ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | wch | . . 3 wff 𝜒 | |
4 | 1, 2, 3 | w3o 1030 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 382 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 382 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 195 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff setvar class |
This definition is referenced by: 3orass 1034 3orrot 1037 3anor 1047 3ioran 1049 3orbi123i 1245 3ori 1380 3jao 1381 mpjao3dan 1387 3orbi123d 1390 3orim123d 1399 3or6 1402 cadan 1539 nf3or 1823 nf3orOLD 2233 eueq3 3348 sspsstri 3671 eltpg 4174 rextpg 4184 tppreqb 4277 somo 4993 ordtri1 5673 ordtri3OLD 5677 ordeleqon 6880 bropopvvv 7142 soxp 7177 swoso 7662 en3lplem2 8395 cflim2 8968 entric 9258 entri2 9259 psslinpr 9732 ssxr 9986 relin01 10431 elznn0nn 11268 nn01to3 11657 xrnemnf 11827 xrnepnf 11828 xrsupss 12011 xrinfmss 12012 swrdnd 13284 cshwshashlem1 15640 tosso 16859 pmltpc 23026 dyaddisj 23170 legso 25294 lnhl 25310 cgracol 25519 colinearalg 25590 clwwlknprop 26300 2wlkonot3v 26402 2spthonot3v 26403 1to3vfriswmgra 26534 3o1cs 28693 3o2cs 28694 3o3cs 28695 tlt3 28996 3orel3 30848 3pm3.2ni 30849 3orit 30851 soseq 30995 nobnddown 31100 mblfinlem2 32617 ts3or1 33130 ts3or2 33131 ts3or3 33132 3orrabdioph 36365 frege114d 37069 df3or2 37079 andi3or 37340 uneqsn 37341 clsk1indlem3 37361 sbc3or 37759 sbc3orgOLD 37763 en3lplem2VD 38101 3orbi123VD 38107 sbc3orgVD 38108 el1fzopredsuc 39948 1to3vfriswmgr 41450 |
Copyright terms: Public domain | W3C validator |