![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > olc | Structured version Visualization version GIF 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 862 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 846 |
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 206 df-or 847 |
This theorem is referenced by: pm1.4 868 pm2.46 882 norbi 886 pm2.07 902 pm2.41 907 pm1.5 919 biorf 936 pm4.72 949 jaob 961 pm3.48 963 andi 1007 dedlemb 1046 consensus 1052 anifp 1071 cad1 1619 19.33 1888 19.33b 1889 dfsb2 2493 mooran2 2551 undif4 4466 prel12g 4864 ordssun 6464 tpres 7199 frxp 8109 frxp2 8127 frxp3 8134 omopth2 8581 naddunif 8689 swoord1 8731 swoord2 8732 fpwwe2lem11 10633 ltapr 11037 zmulcl 12608 nn0lt2 12622 elnn1uz2 12906 mnflt 13100 mnfltpnf 13103 fzm1 13578 expeq0 14055 zzlesq 14167 swrdnnn0nd 14603 nn0o1gt2 16321 prm23lt5 16744 vdwlem9 16919 cshwshashlem1 17026 cshwshash 17035 funcres2c 17849 tsrlemax 18536 odlem1 19398 gexlem1 19442 0top 22478 cmpfi 22904 alexsubALTlem3 23545 dyadmbl 25109 plydivex 25802 scvxcvx 26480 gausslemma2dlem0f 26854 nb3grprlem1 28627 1to3vfriswmgr 29523 frgrwopreg 29566 frgrregorufr 29568 frgrregord13 29639 disjunsn 31813 dfon2lem4 34747 dfrdg4 34912 broutsideof2 35083 lineunray 35108 fwddifnp1 35126 meran1 35285 bj-orim2 35421 bj-peircecurry 35423 bj-falor2 35452 bj-sbsb 35704 bj-unrab 35795 wl-orel12 36369 tsor3 37006 paddclN 38702 lcfl6 40360 sbor2 41024 fsuppind 41160 omcl3g 42070 ifpid3g 42229 ifpim4 42235 rp-fakeanorass 42250 sqrtcval 42378 iunrelexp0 42439 clsk1indlem3 42780 19.33-2 43127 ax6e2ndeq 43306 undif3VD 43629 ax6e2ndeqVD 43656 ax6e2ndeqALT 43678 stoweidlem26 44729 stoweidlem37 44740 fourierswlem 44933 fouriersw 44934 elaa2lem 44936 salexct 45037 sge0z 45078 nfunsnafv2 45920 prproropf1olem4 46161 sfprmdvdsmersenne 46258 nn0o1gt2ALTV 46349 odd2prm2 46373 even3prm2 46374 stgoldbwt 46431 nrhmzr 46634 reorelicc 47350 rrx2plord2 47362 line2y 47395 |
Copyright terms: Public domain | W3C validator |