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 859 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 843 |
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 209 df-or 844 |
This theorem is referenced by: pm1.4 865 pm2.46 879 norbi 883 pm2.07 899 pm2.41 904 pm1.5 916 biorf 933 pm4.72 946 jaob 958 pm3.48 960 andi 1004 dedlemb 1041 consensus 1047 anifp 1065 norassOLD 1534 cad1 1617 19.33 1885 19.33b 1886 dfsb2 2532 dfsb2ALT 2591 mooran2 2640 undif4 4416 prel12g 4794 ordssun 6290 tpres 6963 frxp 7820 omopth2 8210 swoord1 8320 swoord2 8321 fpwwe2lem12 10063 ltapr 10467 zmulcl 12032 nn0lt2 12046 elnn1uz2 12326 mnflt 12519 mnfltpnf 12522 fzm1 12988 expeq0 13460 swrdnnn0nd 14018 nn0o1gt2 15732 prm23lt5 16151 vdwlem9 16325 cshwshashlem1 16429 cshwshash 16438 funcres2c 17171 tsrlemax 17830 odlem1 18663 gexlem1 18704 0top 21591 cmpfi 22016 alexsubALTlem3 22657 dyadmbl 24201 plydivex 24886 scvxcvx 25563 gausslemma2dlem0f 25937 nb3grprlem1 27162 1to3vfriswmgr 28059 frgrwopreg 28102 frgrregorufr 28104 frgrregord13 28175 disjunsn 30344 dfon2lem4 33031 dfrdg4 33412 broutsideof2 33583 lineunray 33608 fwddifnp1 33626 meran1 33759 bj-orim2 33891 bj-peircecurry 33893 bj-falor2 33919 bj-sbsb 34160 bj-unrab 34247 wl-orel12 34766 tsor3 35442 paddclN 36993 lcfl6 38651 sbor2 39123 ifpid3g 39878 ifpim4 39884 rp-fakeanorass 39899 iunrelexp0 40067 clsk1indlem3 40413 19.33-2 40734 ax6e2ndeq 40913 undif3VD 41236 ax6e2ndeqVD 41263 ax6e2ndeqALT 41285 stoweidlem26 42331 stoweidlem37 42342 fourierswlem 42535 fouriersw 42536 elaa2lem 42538 salexct 42637 sge0z 42677 nfunsnafv2 43444 prproropf1olem4 43688 sfprmdvdsmersenne 43788 nn0o1gt2ALTV 43879 odd2prm2 43903 even3prm2 43904 stgoldbwt 43961 nrhmzr 44164 reorelicc 44717 rrx2plord2 44729 line2y 44762 |
Copyright terms: Public domain | W3C validator |