![]() |
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 919. (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 1083 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 844 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 844 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 209 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff setvar class |
This definition is referenced by: 3orass 1087 3orrot 1089 3ioran 1103 3ianor 1104 3orbi123i 1153 3ori 1421 3jao 1422 mpjao3danOLD 1429 3orbi123d 1432 3orim123d 1441 3or6 1444 cadan 1611 nf3or 1906 eueq3 3650 sspsstri 4030 eltpg 4583 rextpg 4595 tppreqb 4698 somo 5474 ordtri1 6192 ordeleqon 7483 bropopvvv 7768 soxp 7806 swoso 8305 en3lplem2 9060 cflim2 9674 entric 9968 entri2 9969 psslinpr 10442 ssxr 10699 relin01 11153 elznn0nn 11983 nn01to3 12329 xrnemnf 12500 xrnepnf 12501 xrsupss 12690 xrinfmss 12691 swrdnd 14007 swrdnnn0nd 14009 swrdnd0 14010 cshwshashlem1 16421 tosso 17638 pmltpc 24054 dyaddisj 24200 legso 26393 lnhl 26409 cgracol 26622 colinearalg 26704 1to3vfriswmgr 28065 3o1cs 30233 3o2cs 30234 3o3cs 30235 fzone1 30549 tlt3 30678 cycpmco2 30825 3orel3 33055 3pm3.2ni 33056 3orit 33058 soseq 33209 nosepdmlem 33300 wl-df2-3mintru2 34902 mblfinlem2 35095 ts3or1 35591 ts3or2 35592 ts3or3 35593 3orrabdioph 39724 frege114d 40459 df3or2 40469 andi3or 40725 uneqsn 40726 clsk1indlem3 40746 sbc3or 41238 en3lplem2VD 41550 3orbi123VD 41556 sbc3orgVD 41557 sbcoreleleqVD 41565 el1fzopredsuc 43882 even3prm2 44237 reorelicc 45124 |
Copyright terms: Public domain | W3C validator |