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 762. (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 972 | . 2 |
5 | 1, 2 | wo 703 | . . 3 |
6 | 5, 3 | wo 703 | . 2 |
7 | 4, 6 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 3orass 976 3orrot 979 3ioran 988 3orbi123i 1184 3ori 1295 3jao 1296 mpjao3dan 1302 3orbi123d 1306 3orim123d 1315 3or6 1318 ecase23d 1345 hb3or 1542 eueq3dc 2904 eltpg 3626 rextpg 3635 nntri3or 6470 nntri1 6473 nnsseleq 6478 elznn0nn 9215 zleloe 9248 uzm1 9506 xrnemnf 9723 xrnepnf 9724 xrltso 9742 hashfiv01gt1 10705 prm23ge5 12207 bd3or 13826 triap 14023 |
Copyright terms: Public domain | W3C validator |