![]() |
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 1053 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 382 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 382 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 196 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff setvar class |
This definition is referenced by: 3orass 1057 3orrot 1061 3anorOLD 1072 3ioran 1073 3ianor 1074 3orbi123i 1271 3ori 1428 3jao 1429 mpjao3dan 1435 3orbi123d 1438 3orim123d 1447 3or6 1450 cadan 1588 nf3or 1875 nf3orOLD 2281 eueq3 3414 sspsstri 3742 eltpg 4259 rextpg 4269 tppreqb 4368 somo 5098 ordtri1 5794 ordtri3OLD 5798 ordeleqon 7030 bropopvvv 7300 soxp 7335 swoso 7820 en3lplem2 8550 cflim2 9123 entric 9417 entri2 9418 psslinpr 9891 ssxr 10145 relin01 10590 elznn0nn 11429 nn01to3 11819 xrnemnf 11989 xrnepnf 11990 xrsupss 12177 xrinfmss 12178 swrdnd 13478 cshwshashlem1 15849 tosso 17083 pmltpc 23265 dyaddisj 23410 legso 25539 lnhl 25555 cgracol 25764 colinearalg 25835 1to3vfriswmgr 27260 3o1cs 29437 3o2cs 29438 3o3cs 29439 tlt3 29793 3orel3 31719 3pm3.2ni 31720 3orit 31722 soseq 31879 nosepdmlem 31958 mblfinlem2 33577 ts3or1 34090 ts3or2 34091 ts3or3 34092 3orrabdioph 37664 frege114d 38367 df3or2 38377 andi3or 38637 uneqsn 38638 clsk1indlem3 38658 sbc3or 39055 sbc3orgOLD 39059 en3lplem2VD 39393 3orbi123VD 39399 sbc3orgVD 39400 el1fzopredsuc 41660 even3prm2 41953 |
Copyright terms: Public domain | W3C validator |