![]() |
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 768. (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 979 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | wo 709 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | wo 709 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 3orass 983 3orrot 986 3ioran 995 3orbi123i 1191 3ori 1311 3jao 1312 mpjao3dan 1318 3orbi123d 1322 3orim123d 1331 3or6 1334 ecase23d 1361 hb3or 1560 eueq3dc 2926 eltpg 3652 rextpg 3661 nntri3or 6518 nntri1 6521 nnsseleq 6526 elznn0nn 9297 zleloe 9330 uzm1 9588 xrnemnf 9807 xrnepnf 9808 xrltso 9826 hashfiv01gt1 10794 prm23ge5 12296 bd3or 15039 triap 15236 |
Copyright terms: Public domain | W3C validator |