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 757. (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 962 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 698 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 698 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 104 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3orass 966 3orrot 969 3ioran 978 3orbi123i 1172 3ori 1282 3jao 1283 mpjao3dan 1289 3orbi123d 1293 3orim123d 1302 3or6 1305 ecase23d 1332 hb3or 1529 eueq3dc 2886 eltpg 3606 rextpg 3615 nntri3or 6443 nntri1 6446 nnsseleq 6451 elznn0nn 9187 zleloe 9220 uzm1 9475 xrnemnf 9691 xrnepnf 9692 xrltso 9710 hashfiv01gt1 10668 prm23ge5 12155 bd3or 13501 triap 13697 |
Copyright terms: Public domain | W3C validator |