Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-3or | Unicode 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 741. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
df-3or |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | wps | . . 3 | |
3 | wch | . . 3 | |
4 | 1, 2, 3 | w3o 946 | . 2 |
5 | 1, 2 | wo 682 | . . 3 |
6 | 5, 3 | wo 682 | . 2 |
7 | 4, 6 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 3orass 950 3orrot 953 3ioran 962 3orbi123i 1156 3ori 1263 3jao 1264 mpjao3dan 1270 3orbi123d 1274 3orim123d 1283 3or6 1286 ecase23d 1313 hb3or 1513 eueq3dc 2831 eltpg 3539 rextpg 3547 nntri3or 6357 nntri1 6360 nnsseleq 6365 elznn0nn 9026 zleloe 9059 uzm1 9312 xrnemnf 9519 xrnepnf 9520 xrltso 9537 hashfiv01gt1 10483 bd3or 12923 triap 13120 |
Copyright terms: Public domain | W3C validator |