![]() |
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 725. (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 929 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | wo 670 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | wo 670 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 3orass 933 3orrot 936 3ioran 945 3orbi123i 1139 3ori 1246 3jao 1247 mpjao3dan 1253 3orbi123d 1257 3orim123d 1266 3or6 1269 ecase23d 1296 hb3or 1496 eueq3dc 2811 eltpg 3516 rextpg 3524 nntri3or 6319 nntri1 6322 nnsseleq 6327 elznn0nn 8920 zleloe 8953 uzm1 9206 xrnemnf 9405 xrnepnf 9406 xrltso 9423 hashfiv01gt1 10369 bd3or 12608 triap 12808 |
Copyright terms: Public domain | W3C validator |