![]() |
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 717. (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 919 | . 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
5 | 1, 2 | wo 662 | . . 3 wff (𝜑 ∨ 𝜓) |
6 | 5, 3 | wo 662 | . 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒) |
7 | 4, 6 | wb 103 | 1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3orass 923 3orrot 926 3ioran 935 3orbi123i 1129 3ori 1232 3jao 1233 mpjao3dan 1239 3orbi123d 1243 3orim123d 1252 3or6 1255 ecase23d 1282 hb3or 1482 eueq3dc 2767 eltpg 3440 rextpg 3448 nntri3or 6130 nntri1 6133 nnsseleq 6138 elznn0nn 8435 zleloe 8468 uzm1 8719 xrnemnf 8918 xrnepnf 8919 xrltso 8936 sizefiv01gt1 9795 bd3or 10763 |
Copyright terms: Public domain | W3C validator |