| 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 769. (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 980 |
. 2
|
| 5 | 1, 2 | wo 710 |
. . 3
|
| 6 | 5, 3 | wo 710 |
. 2
|
| 7 | 4, 6 | wb 105 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: 3orass 984 3orrot 987 3ioran 996 3orbi123i 1192 3ori 1313 3jao 1314 mpjao3dan 1320 3orbi123d 1324 3orim123d 1333 3or6 1336 ecase23d 1363 hb3or 1572 eueq3dc 2947 eltpg 3678 rextpg 3687 nntri3or 6579 nntri1 6582 nnsseleq 6587 elznn0nn 9386 zleloe 9419 uzm1 9679 xrnemnf 9899 xrnepnf 9900 xrltso 9918 hashfiv01gt1 10927 swrdnd 11112 prm23ge5 12587 bd3or 15765 triap 15968 |
| Copyright terms: Public domain | W3C validator |