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 918. (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 1082 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 843 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 843 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 208 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff setvar class |
This definition is referenced by: 3orass 1086 3orrot 1088 3ioran 1102 3ianor 1103 3orbi123i 1152 3ori 1420 3jao 1421 mpjao3danOLD 1428 3orbi123d 1431 3orim123d 1440 3or6 1443 cadan 1610 nf3or 1906 eueq3 3702 sspsstri 4079 eltpg 4623 rextpg 4635 tppreqb 4738 somo 5510 ordtri1 6224 ordeleqon 7503 bropopvvv 7785 soxp 7823 swoso 8322 en3lplem2 9076 cflim2 9685 entric 9979 entri2 9980 psslinpr 10453 ssxr 10710 relin01 11164 elznn0nn 11996 nn01to3 12342 xrnemnf 12513 xrnepnf 12514 xrsupss 12703 xrinfmss 12704 swrdnd 14016 swrdnnn0nd 14018 swrdnd0 14019 cshwshashlem1 16429 tosso 17646 pmltpc 24051 dyaddisj 24197 legso 26385 lnhl 26401 cgracol 26614 colinearalg 26696 1to3vfriswmgr 28059 3o1cs 30227 3o2cs 30228 3o3cs 30229 fzone1 30523 tlt3 30652 cycpmco2 30775 3orel3 32942 3pm3.2ni 32943 3orit 32945 soseq 33096 nosepdmlem 33187 mblfinlem2 34945 ts3or1 35446 ts3or2 35447 ts3or3 35448 3orrabdioph 39429 frege114d 40152 df3or2 40162 andi3or 40421 uneqsn 40422 clsk1indlem3 40442 sbc3or 40915 en3lplem2VD 41227 3orbi123VD 41233 sbc3orgVD 41234 sbcoreleleqVD 41242 el1fzopredsuc 43574 even3prm2 43933 reorelicc 44746 |
Copyright terms: Public domain | W3C validator |