![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orrd | Structured version Visualization version Unicode 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 380 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 190 df-or 376 |
This theorem is referenced by: olc 390 orc 391 pm2.68 416 pm4.79 591 19.30 1754 axi12 2439 axbnd 2440 sspss 3543 pwpw0 4132 sssn 4142 pwsnALT 4206 unissint 4272 disjxiun 4412 pwssun 4758 ordtr3 5486 ordtri2or 5536 unizlim 5557 fvclss 6171 orduniorsuc 6683 ordzsl 6698 nn0suc 6743 xpexr 6759 odi 7305 swoso 7419 erdisj 7436 ordtypelem7 8064 wemapsolem 8090 domwdom 8114 iscard3 8549 ackbij1lem18 8692 fin56 8848 entric 9007 gchdomtri 9079 inttsk 9224 r1tskina 9232 psslinpr 9481 ssxr 9728 letric 9759 mul0or 10279 mulge0b 10502 zeo 11049 uzm1 11217 xrletri 11478 supxrgtmnf 11643 sq01 12425 ruclem3 14333 phiprmpw 14772 pleval2i 16258 irredn0 17979 drngmul0or 18044 lvecvs0or 18379 lssvs0or 18381 lspsnat 18416 lsppratlem1 18418 domnchr 19151 fctop 20067 cctop 20069 ppttop 20070 clslp 20212 restntr 20246 cnconn 20485 txindis 20697 txcon 20752 isufil2 20971 ufprim 20972 alexsubALTlem3 21112 pmltpc 22449 iundisj2 22550 limcco 22896 fta1b 23168 aalioulem2 23337 abelthlem2 23435 logreclem 23747 dchrfi 24231 2sqb 24354 tgbtwnconn1 24668 legov3 24691 coltr 24740 colline 24742 tglowdim2ln 24744 ragflat3 24799 ragperp 24810 lmieu 24874 lmicom 24878 lmimid 24884 nvmul0or 26321 hvmul0or 26726 atomli 28083 atordi 28085 iundisj2f 28248 iundisj2fi 28421 signsply0 29488 cvmsdisj 30041 nepss 30398 dfon2lem6 30482 soseq 30540 btwnconn1lem13 30914 wl-exeq 31911 lsator0sp 32611 lkreqN 32780 2at0mat0 33134 trlator0 33781 dochkrshp4 35001 dochsat0 35069 lcfl6 35112 rp-fakeimass 36200 frege124d 36397 pm10.57 36763 icccncfext 37802 fourierdlem70 38077 uzlidlring 40201 nneop 40605 |
Copyright terms: Public domain | W3C validator |