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 762. (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 972 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 703 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 703 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 104 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3orass 976 3orrot 979 3ioran 988 3orbi123i 1184 3ori 1295 3jao 1296 mpjao3dan 1302 3orbi123d 1306 3orim123d 1315 3or6 1318 ecase23d 1345 hb3or 1542 eueq3dc 2904 eltpg 3628 rextpg 3637 nntri3or 6472 nntri1 6475 nnsseleq 6480 elznn0nn 9226 zleloe 9259 uzm1 9517 xrnemnf 9734 xrnepnf 9735 xrltso 9753 hashfiv01gt1 10716 prm23ge5 12218 bd3or 13864 triap 14061 |
Copyright terms: Public domain | W3C validator |