![]() |
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 767. (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 977 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 708 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 708 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 105 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3orass 981 3orrot 984 3ioran 993 3orbi123i 1189 3ori 1300 3jao 1301 mpjao3dan 1307 3orbi123d 1311 3orim123d 1320 3or6 1323 ecase23d 1350 hb3or 1549 eueq3dc 2913 eltpg 3639 rextpg 3648 nntri3or 6496 nntri1 6499 nnsseleq 6504 elznn0nn 9269 zleloe 9302 uzm1 9560 xrnemnf 9779 xrnepnf 9780 xrltso 9798 hashfiv01gt1 10764 prm23ge5 12266 bd3or 14666 triap 14862 |
Copyright terms: Public domain | W3C validator |