New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > orc | Unicode version |
Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
orc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.24 101 | . 2 | |
2 | 1 | orrd 367 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wo 357 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-or 359 |
This theorem is referenced by: pm1.4 375 orcd 381 orcs 383 pm2.45 386 pm2.67-2 391 biorfi 396 pm1.5 508 pm2.4 558 pm4.44 560 pm4.45 669 pm3.48 806 orabs 828 andi 837 pm4.72 846 biort 866 pm5.71 902 dedlema 920 consensus 925 3mix1 1124 cad1 1398 cad11 1399 cad0 1400 19.33 1607 19.33b 1608 dfsb2 2055 moor 2257 ssun1 3426 undif3 3515 reuun1 3537 phiall 4618 clos1basesuc 5882 leconnnc 6218 ncslesuc 6267 nchoicelem9 6297 |
Copyright terms: Public domain | W3C validator |