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 756. (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 961 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 697 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 697 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 104 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3orass 965 3orrot 968 3ioran 977 3orbi123i 1171 3ori 1278 3jao 1279 mpjao3dan 1285 3orbi123d 1289 3orim123d 1298 3or6 1301 ecase23d 1328 hb3or 1528 eueq3dc 2858 eltpg 3569 rextpg 3577 nntri3or 6389 nntri1 6392 nnsseleq 6397 elznn0nn 9068 zleloe 9101 uzm1 9356 xrnemnf 9564 xrnepnf 9565 xrltso 9582 hashfiv01gt1 10528 bd3or 13027 triap 13224 |
Copyright terms: Public domain | W3C validator |