![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orrd | Structured version Visualization version GIF version |
Description: Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.) |
Ref | Expression |
---|---|
orrd.1 | ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
Ref | Expression |
---|---|
orrd | ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orrd.1 | . 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) | |
2 | pm2.54 851 | . 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒)) | |
3 | 1, 2 | syl 17 | 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: orc 866 olc 867 pm2.68 900 pm4.79 1003 19.30 1885 axi12 2702 r19.30 3121 r19.30OLD 3122 sspss 4097 eqoreldif 4684 pwpw0 4812 sssn 4825 pwsnOLD 4897 unissint 4972 disjiund 5134 disjxiun 5141 otsndisj 5515 otiunsndisj 5516 pwssun 5567 isso2i 5619 ordtr3 6401 ordtri2or 6454 unizlim 6479 fvclss 7228 orduniorsuc 7805 ordzsl 7821 nn0suc 7873 xpexr 7896 soseq 8132 odi 8567 swoso 8724 erdisj 8743 ordtypelem7 9506 wemapsolem 9532 domwdom 9556 iscard3 10075 ackbij1lem18 10219 fin56 10375 entric 10539 gchdomtri 10611 inttsk 10756 r1tskina 10764 psslinpr 11013 ssxr 11270 letric 11301 mul0or 11841 mulge0b 12071 zeo 12635 uzm1 12847 xrletri 13119 supxrgtmnf 13295 sq01 14175 ruclem3 16163 prm2orodd 16615 phiprmpw 16696 pleval2i 18276 irredn0 20215 drngmul0or 20321 lvecvs0or 20698 lssvs0or 20700 lspsnat 20735 lsppratlem1 20737 domnchr 21057 fctop 22476 cctop 22478 ppttop 22479 clslp 22621 restntr 22655 cnconn 22895 txindis 23107 txconn 23162 isufil2 23381 ufprim 23382 alexsubALTlem3 23522 pmltpc 24936 iundisj2 25035 limcco 25379 fta1b 25656 aalioulem2 25815 abelthlem2 25913 logreclem 26234 dchrfi 26725 2sqb 26902 nosepdmlem 27153 noetasuplem4 27206 sletric 27234 tgbtwnconn1 27793 legov3 27816 coltr 27865 colline 27867 tglowdim2ln 27869 ragflat3 27924 ragperp 27935 lmieu 28002 lmicom 28006 lmimid 28012 numedglnl 28371 nvmul0or 29868 hvmul0or 30243 atomli 31600 atordi 31602 iundisj2f 31787 iundisj2fi 31979 mxidlprm 32537 ssmxidl 32539 qsdrng 32557 zarclssn 32784 signsply0 33493 pthisspthorcycl 34050 cvmsdisj 34192 nepss 34618 dfon2lem6 34691 btwnconn1lem13 35002 wl-exeq 36308 eqvreldisj 37390 lsator0sp 37777 lkreqN 37946 2at0mat0 38302 trlator0 38948 dochkrshp4 40166 dochsat0 40234 lcfl6 40277 rp-fakeimass 42134 frege124d 42383 clsk1independent 42668 mnringmulrcld 42858 pm10.57 43001 icccncfext 44476 fourierdlem70 44765 ichnreuop 46013 uzlidlring 46667 nneop 47052 mo0sn 47340 |
Copyright terms: Public domain | W3C validator |