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 863 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 847 |
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 210 df-or 848 |
This theorem is referenced by: pm1.4 869 pm2.46 883 norbi 887 pm2.07 903 pm2.41 908 pm1.5 920 biorf 937 pm4.72 950 jaob 962 pm3.48 964 andi 1008 dedlemb 1047 consensus 1053 anifp 1072 norassOLD 1540 cad1 1624 19.33 1892 19.33b 1893 dfsb2 2496 mooran2 2555 undif4 4378 prel12g 4771 ordssun 6309 tpres 7013 frxp 7890 omopth2 8309 swoord1 8419 swoord2 8420 fpwwe2lem11 10252 ltapr 10656 zmulcl 12223 nn0lt2 12237 elnn1uz2 12518 mnflt 12712 mnfltpnf 12715 fzm1 13189 expeq0 13662 swrdnnn0nd 14218 nn0o1gt2 15939 prm23lt5 16364 vdwlem9 16539 cshwshashlem1 16646 cshwshash 16655 funcres2c 17405 tsrlemax 18089 odlem1 18924 gexlem1 18965 0top 21877 cmpfi 22302 alexsubALTlem3 22943 dyadmbl 24494 plydivex 25187 scvxcvx 25865 gausslemma2dlem0f 26239 nb3grprlem1 27465 1to3vfriswmgr 28360 frgrwopreg 28403 frgrregorufr 28405 frgrregord13 28476 disjunsn 30649 dfon2lem4 33478 frxp2 33525 frxp3 33531 dfrdg4 33987 broutsideof2 34158 lineunray 34183 fwddifnp1 34201 meran1 34334 bj-orim2 34470 bj-peircecurry 34472 bj-falor2 34501 bj-sbsb 34754 bj-unrab 34848 wl-orel12 35404 tsor3 36042 paddclN 37591 lcfl6 39249 sbor2 39897 fsuppind 39987 ifpid3g 40782 ifpim4 40788 rp-fakeanorass 40803 sqrtcval 40923 iunrelexp0 40985 clsk1indlem3 41328 19.33-2 41671 ax6e2ndeq 41850 undif3VD 42173 ax6e2ndeqVD 42200 ax6e2ndeqALT 42222 stoweidlem26 43240 stoweidlem37 43251 fourierswlem 43444 fouriersw 43445 elaa2lem 43447 salexct 43546 sge0z 43586 nfunsnafv2 44387 prproropf1olem4 44629 sfprmdvdsmersenne 44726 nn0o1gt2ALTV 44817 odd2prm2 44841 even3prm2 44842 stgoldbwt 44899 nrhmzr 45102 reorelicc 45727 rrx2plord2 45739 line2y 45772 |
Copyright terms: Public domain | W3C validator |