![]() |
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 392 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 382 |
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 197 df-or 384 |
This theorem is referenced by: pm1.4 400 pm2.07 410 pm2.46 412 biorf 419 pm1.5 545 pm2.41 598 jaob 857 pm3.48 914 norbi 940 andi 947 pm4.72 956 annotanannotOLD 978 dedlemb 1033 consensus 1041 anifp 1058 cad1 1692 nfntht 1856 nfntht2 1857 19.33 1949 19.33b 1950 dfsb2 2498 mooran2 2654 undif3OLD 4020 undif4 4167 prel12g 4532 ordelinelOLD 5975 ordssun 5976 tpres 6618 frxp 7443 omopth2 7821 swoord1 7930 swoord2 7931 rankxplim3 8905 fpwwe2lem12 9626 ltapr 10030 zmulcl 11589 nn0lt2 11603 elnn1uz2 11929 mnflt 12121 mnfltpnf 12124 fzm1 12584 expeq0 13055 nn0o1gt2 15270 prm23lt5 15692 vdwlem9 15866 cshwshashlem1 15975 cshwshash 15984 funcres2c 16733 tsrlemax 17392 odlem1 18125 gexlem1 18165 0top 20960 cmpfi 21384 alexsubALTlem3 22025 dyadmbl 23539 plydivex 24222 scvxcvx 24882 gausslemma2dlem0f 25256 nb3grprlem1 26451 1to3vfriswmgr 27405 frgrwopreg 27448 frgrregorufr 27450 frgrregord13 27535 disjunsn 29685 dfon2lem4 31967 dfrdg4 32335 broutsideof2 32506 lineunray 32531 fwddifnp1 32549 meran1 32687 bj-orim2 32818 bj-currypeirce 32821 bj-peircecurry 32822 bj-falor2 32847 bj-sbsb 33101 bj-unrab 33199 wl-orel12 33576 tsor3 34238 paddclN 35600 lcfl6 37260 ifpid3g 38308 ifpim4 38314 rp-fakeanorass 38329 iunrelexp0 38465 clsk1indlem3 38812 19.33-2 39052 ax6e2ndeq 39246 undif3VD 39586 ax6e2ndeqVD 39613 ax6e2ndeqALT 39635 disjxp1 39706 stoweidlem26 40715 stoweidlem37 40726 fourierswlem 40919 fouriersw 40920 elaa2lem 40922 salexct 41024 sge0z 41064 sfprmdvdsmersenne 41999 nn0o1gt2ALTV 42084 odd2prm2 42106 even3prm2 42107 stgoldbwt 42143 nrhmzr 42352 |
Copyright terms: Public domain | W3C validator |