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 389 | . 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 383 |
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 385 |
This theorem is referenced by: olc 399 orc 400 pm2.68 426 pm4.79 607 19.30 1809 axi12 2600 axbnd 2601 sspss 3706 eqoreldif 4225 pwpw0 4344 sssn 4358 pwsnALT 4429 unissint 4501 disjiund 4643 disjxiun 4649 disjxiunOLD 4650 otsndisj 4979 otiunsndisj 4980 pwssun 5020 isso2i 5067 ordtr3 5769 ordtr3OLD 5770 ordtri2or 5822 unizlim 5844 fvclss 6500 orduniorsuc 7030 ordzsl 7045 nn0suc 7090 xpexr 7106 odi 7659 swoso 7775 erdisj 7794 ordtypelem7 8429 wemapsolem 8455 domwdom 8479 iscard3 8916 ackbij1lem18 9059 fin56 9215 entric 9379 gchdomtri 9451 inttsk 9596 r1tskina 9604 psslinpr 9853 ssxr 10107 letric 10137 mul0or 10667 mulge0b 10893 zeo 11463 uzm1 11718 xrletri 11984 supxrgtmnf 12159 sq01 12986 ruclem3 14962 prm2orodd 15404 phiprmpw 15481 pleval2i 16964 irredn0 18703 drngmul0or 18768 lvecvs0or 19108 lssvs0or 19110 lspsnat 19145 lsppratlem1 19147 domnchr 19880 fctop 20808 cctop 20810 ppttop 20811 clslp 20952 restntr 20986 cnconn 21225 txindis 21437 txconn 21492 isufil2 21712 ufprim 21713 alexsubALTlem3 21853 pmltpc 23219 iundisj2 23317 limcco 23657 fta1b 23929 aalioulem2 24088 abelthlem2 24186 logreclem 24500 dchrfi 24980 2sqb 25157 tgbtwnconn1 25470 legov3 25493 coltr 25542 colline 25544 tglowdim2ln 25546 ragflat3 25601 ragperp 25612 lmieu 25676 lmicom 25680 lmimid 25686 numedglnl 26039 nvmul0or 27505 hvmul0or 27882 atomli 29241 atordi 29243 iundisj2f 29403 iundisj2fi 29556 signsply0 30628 cvmsdisj 31252 nepss 31599 dfon2lem6 31693 soseq 31751 nosepdmlem 31833 noetalem3 31865 btwnconn1lem13 32206 wl-exeq 33321 lsator0sp 34288 lkreqN 34457 2at0mat0 34811 trlator0 35458 dochkrshp4 36678 dochsat0 36746 lcfl6 36789 rp-fakeimass 37857 frege124d 38053 clsk1independent 38344 pm10.57 38570 icccncfext 40100 fourierdlem70 40393 uzlidlring 41929 nneop 42320 |
Copyright terms: Public domain | W3C validator |