![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > olc | Structured version Visualization version Unicode version |
Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
olc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 6 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | orrd 380 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 189 df-or 372 |
This theorem is referenced by: pm1.4 388 pm2.07 398 pm2.46 400 biorf 407 pm1.5 525 pm2.41 577 jaob 792 pm3.48 844 norbi 870 andi 878 pm4.72 887 dedlemb 966 consensus 970 anifp 1433 cad1 1519 19.33 1747 19.33b 1748 dfsb2 2202 mooran2 2357 undif3 3704 undif4 3821 ordelinel 5521 ordssun 5522 ordequn 5523 tpres 6117 frxp 6906 omopth2 7285 swoord1 7392 swoord2 7393 rankxplim3 8352 fpwwe2lem12 9066 ltapr 9470 zmulcl 10985 nn0lt2 11000 elnn1uz2 11235 mnflt 11425 mnfltpnf 11428 fzm1 11874 expeq0 12302 vdwlem9 14939 cshwshashlem1 15066 cshwshash 15075 funcres2c 15806 tsrlemax 16466 odlem1 17181 odlem1OLD 17184 gexlem1 17228 gexlem1OLD 17230 0top 19999 cmpfi 20423 alexsubALTlem3 21064 dyadmbl 22558 plydivex 23250 scvxcvx 23911 nb3graprlem1 25179 uvtx01vtx 25220 1to3vfriswmgra 25735 frgraregorufr 25781 frgraregord13 25847 disjunsn 28204 dfon2lem4 30432 sltsgn1 30548 sltsgn2 30549 dfrdg4 30718 broutsideof2 30889 lineunray 30914 fwddifnp1 30932 meran1 31071 bj-falor2 31169 bj-nfntht 31196 bj-nfntht2 31197 bj-unrab 31529 wl-orel12 31849 tsor3 32391 prtlem90 32431 paddclN 33407 lcfl6 35068 ifpid3g 36136 ifpim4 36142 rp-fakeanorass 36157 iunrelexp0 36294 19.33-2 36731 ax6e2ndeq 36926 undif3VD 37279 ax6e2ndeqVD 37306 ax6e2ndeqALT 37328 disjxp1 37411 stoweidlem26 37886 stoweidlem37 37898 fourierswlem 38094 fouriersw 38095 elaa2lem 38097 elaa2lemOLD 38098 salexct 38193 sge0z 38217 nnfoctbdjlem 38293 nn0o1gt2ALTV 38823 stgoldbwt 38877 nb3grprlem1 39454 nrhmzr 39926 nn0o1gt2 40380 |
Copyright terms: Public domain | W3C validator |