![]() |
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 1085 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 844 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 844 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 205 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff setvar class |
This definition is referenced by: 3orass 1089 3orrot 1091 3ioran 1105 3ianor 1106 3orbi123i 1155 3ori 1423 3jao 1424 mpjao3danOLD 1431 3orbi123d 1434 3orim123d 1443 3or6 1446 3orel3 1485 3pm3.2ni 1487 cadan 1609 nf3or 1907 eueq3 3707 sspsstri 4102 eltpg 4689 rextpg 4703 tppreqb 4808 somo 5625 ordtri1 6397 ordeleqon 7773 bropopvvv 8081 soxp 8120 soseq 8150 swoso 8742 fsetexb 8864 en3lplem2 9614 cflim2 10264 entric 10558 entri2 10559 psslinpr 11032 ssxr 11290 relin01 11745 elznn0nn 12579 nn01to3 12932 xrnemnf 13104 xrnepnf 13105 xrsupss 13295 xrinfmss 13296 swrdnd 14611 swrdnnn0nd 14613 swrdnd0 14614 cshwshashlem1 17036 tosso 18382 pmltpc 25299 dyaddisj 25445 nosepdmlem 27530 mulsproplem13 27942 mulsproplem14 27943 legso 28284 lnhl 28300 cgracol 28513 colinearalg 28602 1to3vfriswmgr 29967 3o1cs 32137 3o2cs 32138 3o3cs 32139 fzone1 32445 tlt3 32574 cycpmco2 32729 3orit 35156 wl-df2-3mintru2 36832 mblfinlem2 36992 ts3or1 37487 ts3or2 37488 ts3or3 37489 3orrabdioph 41986 oneptri 42471 frege114d 42974 df3or2 42984 andi3or 43240 uneqsn 43241 clsk1indlem3 43259 sbc3or 43758 en3lplem2VD 44070 3orbi123VD 44076 sbc3orgVD 44077 sbcoreleleqVD 44085 el1fzopredsuc 46494 even3prm2 46848 reorelicc 47560 |
Copyright terms: Public domain | W3C validator |