![]() |
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 905. (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 1067 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 833 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 833 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 198 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff setvar class |
This definition is referenced by: 3orass 1071 3orrot 1073 3ioran 1086 3ianor 1087 3orbi123i 1136 3ori 1404 3jao 1405 mpjao3dan 1411 3orbi123d 1414 3orim123d 1423 3or6 1426 cadan 1572 nf3or 1868 eueq3 3617 sspsstri 3971 eltpg 4498 rextpg 4510 tppreqb 4613 somo 5363 ordtri1 6064 ordeleqon 7321 bropopvvv 7595 soxp 7630 swoso 8124 en3lplem2 8872 cflim2 9485 entric 9779 entri2 9780 psslinpr 10253 ssxr 10512 relin01 10967 elznn0nn 11810 nn01to3 12158 xrnemnf 12332 xrnepnf 12333 xrsupss 12521 xrinfmss 12522 swrdnd 13825 swrdnnn0nd 13827 swrdnd0 13828 cshwshashlem1 16288 tosso 17507 pmltpc 23757 dyaddisj 23903 legso 26090 lnhl 26106 cgracol 26319 colinearalg 26402 1to3vfriswmgr 27817 3o1cs 30011 3o2cs 30012 3o3cs 30013 tlt3 30384 3orel3 32462 3pm3.2ni 32463 3orit 32465 soseq 32617 nosepdmlem 32708 mblfinlem2 34371 ts3or1 34875 ts3or2 34876 ts3or3 34877 3orrabdioph 38776 frege114d 39466 df3or2 39476 andi3or 39735 uneqsn 39736 clsk1indlem3 39756 sbc3or 40285 en3lplem2VD 40597 3orbi123VD 40603 sbc3orgVD 40604 sbcoreleleqVD 40612 el1fzopredsuc 42932 even3prm2 43253 reorelicc 44066 |
Copyright terms: Public domain | W3C validator |