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 915. (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 1078 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 841 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 841 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 207 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff setvar class |
This definition is referenced by: 3orass 1082 3orrot 1084 3ioran 1098 3ianor 1099 3orbi123i 1148 3ori 1416 3jao 1417 mpjao3dan 1423 3orbi123d 1426 3orim123d 1435 3or6 1438 cadan 1601 nf3or 1897 eueq3 3701 sspsstri 4078 eltpg 4617 rextpg 4629 tppreqb 4732 somo 5504 ordtri1 6218 ordeleqon 7491 bropopvvv 7776 soxp 7814 swoso 8312 en3lplem2 9065 cflim2 9674 entric 9968 entri2 9969 psslinpr 10442 ssxr 10699 relin01 11153 elznn0nn 11984 nn01to3 12330 xrnemnf 12502 xrnepnf 12503 xrsupss 12692 xrinfmss 12693 swrdnd 14006 swrdnnn0nd 14008 swrdnd0 14009 cshwshashlem1 16419 tosso 17636 pmltpc 23980 dyaddisj 24126 legso 26313 lnhl 26329 cgracol 26542 colinearalg 26624 1to3vfriswmgr 27987 3o1cs 30155 3o2cs 30156 3o3cs 30157 fzone1 30450 tlt3 30580 cycpmco2 30703 3orel3 32840 3pm3.2ni 32841 3orit 32843 soseq 32994 nosepdmlem 33085 mblfinlem2 34812 ts3or1 35314 ts3or2 35315 ts3or3 35316 3orrabdioph 39260 frege114d 39983 df3or2 39993 andi3or 40252 uneqsn 40253 clsk1indlem3 40273 sbc3or 40746 en3lplem2VD 41058 3orbi123VD 41064 sbc3orgVD 41065 sbcoreleleqVD 41073 el1fzopredsuc 43406 even3prm2 43731 reorelicc 44595 |
Copyright terms: Public domain | W3C validator |