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 967 | . 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 971 3orrot 974 3ioran 983 3orbi123i 1179 3ori 1290 3jao 1291 mpjao3dan 1297 3orbi123d 1301 3orim123d 1310 3or6 1313 ecase23d 1340 hb3or 1537 eueq3dc 2899 eltpg 3620 rextpg 3629 nntri3or 6457 nntri1 6460 nnsseleq 6465 elznn0nn 9201 zleloe 9234 uzm1 9492 xrnemnf 9709 xrnepnf 9710 xrltso 9728 hashfiv01gt1 10691 prm23ge5 12192 bd3or 13671 triap 13868 |
Copyright terms: Public domain | W3C validator |