![]() |
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 547. (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 1071 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 382 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 382 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 196 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff setvar class |
This definition is referenced by: 3orass 1075 3orrot 1077 3anorOLD 1094 3ioran 1095 3ianor 1096 3orbi123i 1159 3ori 1529 3jao 1530 mpjao3dan 1536 3orbi123d 1539 3orim123d 1548 3or6 1551 cadan 1689 nf3or 1976 nf3orOLD 2382 eueq3 3514 sspsstri 3843 eltpg 4363 rextpg 4373 tppreqb 4473 somo 5213 ordtri1 5909 ordtri3OLD 5913 ordeleqon 7145 bropopvvv 7415 soxp 7450 swoso 7936 en3lplem2 8673 cflim2 9269 entric 9563 entri2 9564 psslinpr 10037 ssxr 10291 relin01 10736 elznn0nn 11575 nn01to3 11966 xrnemnf 12136 xrnepnf 12137 xrsupss 12324 xrinfmss 12325 swrdnd 13624 cshwshashlem1 15996 tosso 17229 pmltpc 23411 dyaddisj 23556 legso 25685 lnhl 25701 cgracol 25910 colinearalg 25981 1to3vfriswmgr 27426 3o1cs 29610 3o2cs 29611 3o3cs 29612 tlt3 29966 3orel3 31892 3pm3.2ni 31893 3orit 31895 soseq 32052 nosepdmlem 32131 mblfinlem2 33752 ts3or1 34265 ts3or2 34266 ts3or3 34267 3orrabdioph 37841 frege114d 38544 df3or2 38554 andi3or 38814 uneqsn 38815 clsk1indlem3 38835 sbc3or 39232 sbc3orgOLD 39236 en3lplem2VD 39570 3orbi123VD 39576 sbc3orgVD 39577 el1fzopredsuc 41837 even3prm2 42130 |
Copyright terms: Public domain | W3C validator |