![]() |
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 683. (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 883 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | wo 628 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | wo 628 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wb 98 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 3orass 887 3orrot 890 3ioran 899 3orbi123i 1093 3ori 1194 3jao 1195 mpjao3dan 1201 3orbi123d 1205 3orim123d 1214 3or6 1217 ecase23d 1239 hb3or 1438 eueq3dc 2709 eltpg 3407 rextpg 3415 nntri3or 6011 nntri1 6013 elznn0nn 8035 zleloe 8068 uzm1 8279 xrnemnf 8469 xrnepnf 8470 xrltso 8487 bd3or 9284 |
Copyright terms: Public domain | W3C validator |