| 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 853 | . 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∨ wo 848 |
| 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 207 df-or 849 |
| This theorem is referenced by: orc 868 olc 869 pm2.68 901 pm4.79 1006 19.30 1881 axi12 2706 r19.30 3120 r19.30OLD 3121 sspss 4102 eqoreldif 4685 pwpw0 4813 sssn 4826 unissint 4972 disjiund 5134 disjxiun 5140 otsndisj 5524 otiunsndisj 5525 pwssun 5575 isso2i 5629 ordtr3 6429 ordtri2or 6482 unizlim 6507 fvclss 7261 orduniorsuc 7850 ordzsl 7866 nn0suc 7916 xpexr 7940 soseq 8184 odi 8617 swoso 8779 erdisj 8799 ordtypelem7 9564 wemapsolem 9590 domwdom 9614 iscard3 10133 ackbij1lem18 10276 fin56 10433 entric 10597 gchdomtri 10669 inttsk 10814 r1tskina 10822 psslinpr 11071 ssxr 11330 letric 11361 mul0or 11903 mulge0b 12138 zeo 12704 uzm1 12916 xrletri 13195 supxrgtmnf 13371 sq01 14264 ruclem3 16269 prm2orodd 16728 phiprmpw 16813 pleval2i 18381 irredn0 20423 drngmul0orOLD 20761 lvecvs0or 21110 lssvs0or 21112 lspsnat 21147 lsppratlem1 21149 domnchr 21547 fctop 23011 cctop 23013 ppttop 23014 clslp 23156 restntr 23190 cnconn 23430 txindis 23642 txconn 23697 isufil2 23916 ufprim 23917 alexsubALTlem3 24057 pmltpc 25485 iundisj2 25584 limcco 25928 fta1b 26211 aalioulem2 26375 abelthlem2 26476 logreclem 26805 dchrfi 27299 2sqb 27476 nosepdmlem 27728 noetasuplem4 27781 sletric 27809 muls0ord 28211 tgbtwnconn1 28583 legov3 28606 coltr 28655 colline 28657 tglowdim2ln 28659 ragflat3 28714 ragperp 28725 lmieu 28792 lmicom 28796 lmimid 28802 numedglnl 29161 pthisspthorcycl 29822 nvmul0or 30669 hvmul0or 31044 atomli 32401 atordi 32403 iundisj2f 32603 iundisj2fi 32799 chnind 33001 gsumfs2d 33058 mxidlprm 33498 ssmxidl 33502 qsdrng 33525 zarclssn 33872 signsply0 34566 cvmsdisj 35275 nepss 35718 dfon2lem6 35789 btwnconn1lem13 36100 wl-exeq 37535 eqvreldisj 38615 lsator0sp 39002 lkreqN 39171 2at0mat0 39527 trlator0 40173 dochkrshp4 41391 dochsat0 41459 lcfl6 41502 expeqidd 42360 rp-fakeimass 43525 frege124d 43774 clsk1independent 44059 mnringmulrcld 44247 pm10.57 44390 icccncfext 45902 fourierdlem70 46191 ichnreuop 47459 uzlidlring 48151 nneop 48447 mo0sn 48735 |
| Copyright terms: Public domain | W3C validator |