![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-3or | GIF version |
Description: Define disjunction ('or') of 3 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 768. (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 979 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 709 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 709 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 105 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3orass 983 3orrot 986 3ioran 995 3orbi123i 1191 3ori 1311 3jao 1312 mpjao3dan 1318 3orbi123d 1322 3orim123d 1331 3or6 1334 ecase23d 1361 hb3or 1560 eueq3dc 2926 eltpg 3652 rextpg 3661 nntri3or 6512 nntri1 6515 nnsseleq 6520 elznn0nn 9285 zleloe 9318 uzm1 9576 xrnemnf 9795 xrnepnf 9796 xrltso 9814 hashfiv01gt1 10780 prm23ge5 12282 bd3or 14965 triap 15162 |
Copyright terms: Public domain | W3C validator |