![]() |
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 388 | . 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒)) | |
3 | 1, 2 | syl 17 | 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: olc 398 orc 399 pm2.68 425 pm4.79 606 19.30 1849 axi12 2629 axbnd 2630 sspss 3739 eqoreldif 4257 pwpw0 4376 sssn 4390 pwsnALT 4461 unissint 4533 disjiund 4675 disjxiun 4681 disjxiunOLD 4682 otsndisj 5008 otiunsndisj 5009 pwssun 5049 isso2i 5096 ordtr3 5807 ordtr3OLD 5808 ordtri2or 5860 unizlim 5882 fvclss 6540 orduniorsuc 7072 ordzsl 7087 nn0suc 7132 xpexr 7148 odi 7704 swoso 7820 erdisj 7837 ordtypelem7 8470 wemapsolem 8496 domwdom 8520 iscard3 8954 ackbij1lem18 9097 fin56 9253 entric 9417 gchdomtri 9489 inttsk 9634 r1tskina 9642 psslinpr 9891 ssxr 10145 letric 10175 mul0or 10705 mulge0b 10931 zeo 11501 uzm1 11756 xrletri 12022 supxrgtmnf 12197 sq01 13026 ruclem3 15006 prm2orodd 15451 phiprmpw 15528 pleval2i 17011 irredn0 18749 drngmul0or 18816 lvecvs0or 19156 lssvs0or 19158 lspsnat 19193 lsppratlem1 19195 domnchr 19928 fctop 20856 cctop 20858 ppttop 20859 clslp 21000 restntr 21034 cnconn 21273 txindis 21485 txconn 21540 isufil2 21759 ufprim 21760 alexsubALTlem3 21900 pmltpc 23265 iundisj2 23363 limcco 23702 fta1b 23974 aalioulem2 24133 abelthlem2 24231 logreclem 24545 dchrfi 25025 2sqb 25202 tgbtwnconn1 25515 legov3 25538 coltr 25587 colline 25589 tglowdim2ln 25591 ragflat3 25646 ragperp 25657 lmieu 25721 lmicom 25725 lmimid 25731 numedglnl 26084 nvmul0or 27633 hvmul0or 28010 atomli 29369 atordi 29371 iundisj2f 29529 iundisj2fi 29684 signsply0 30756 cvmsdisj 31378 nepss 31725 dfon2lem6 31817 soseq 31879 nosepdmlem 31958 noetalem3 31990 btwnconn1lem13 32331 wl-exeq 33451 lsator0sp 34606 lkreqN 34775 2at0mat0 35129 trlator0 35776 dochkrshp4 36995 dochsat0 37063 lcfl6 37106 rp-fakeimass 38174 frege124d 38370 clsk1independent 38661 pm10.57 38887 icccncfext 40418 fourierdlem70 40711 uzlidlring 42254 nneop 42645 |
Copyright terms: Public domain | W3C validator |