MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orrd Unicode version

Theorem orrd 378
Description: Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.)
Hypothesis
Ref Expression
orrd.1
Assertion
Ref Expression
orrd

Proof of Theorem orrd
StepHypRef Expression
1 orrd.1 . 2
2 pm2.54 374 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368
This theorem is referenced by:  olc  384  orc  385  pm2.68  410  pm4.79  583  19.30  1692  axi12  2433  axbnd  2434  sspss  3602  pwpw0  4178  sssn  4188  pwsnALT  4244  unissint  4311  disjxiun  4449  pwssun  4791  ordtr3  4928  ordtri2or  4978  unizlim  4999  fvclss  6154  orduniorsuc  6665  ordzsl  6680  nn0suc  6724  xpexr  6740  odi  7247  swoso  7361  erdisj  7378  ordtypelem7  7970  wemapsolem  7996  domwdom  8021  iscard3  8495  ackbij1lem18  8638  fin56  8794  entric  8953  gchdomtri  9028  inttsk  9173  r1tskina  9181  psslinpr  9430  ssxr  9675  letric  9706  mul0or  10214  mulge0b  10437  zeo  10973  uzm1  11140  xrletri  11386  supxrgtmnf  11550  sq01  12288  ruclem3  13966  phiprmpw  14306  pleval2i  15594  irredn0  17352  drngmul0or  17417  lvecvs0or  17754  lssvs0or  17756  lspsnat  17791  lsppratlem1  17793  domnchr  18569  fctop  19505  cctop  19507  ppttop  19508  clslp  19649  restntr  19683  cnconn  19923  txindis  20135  txcon  20190  isufil2  20409  ufprim  20410  alexsubALTlem3  20549  pmltpc  21862  iundisj2  21959  limcco  22297  fta1b  22570  aalioulem2  22729  abelthlem2  22827  logreclem  23150  dchrfi  23530  2sqb  23653  tgbtwnconn1  23962  legov3  23984  coltr  24027  colline  24030  tglowdim2ln  24032  ragflat3  24083  ragperp  24094  lmieu  24150  lmicom  24154  lmimid  24159  nvmul0or  25547  hvmul0or  25942  atomli  27301  atordi  27303  iundisj2f  27449  iundisj2fi  27602  signsply0  28508  cvmsdisj  28715  nepss  29095  dfon2lem6  29220  soseq  29334  btwnconn1lem13  29749  wl-exeq  29987  pm10.57  31276  icccncfext  31690  fourierdlem70  31959  uzlidlring  32735  lsator0sp  34726  lkreqN  34895  2at0mat0  35249  trlator0  35896  dochkrshp4  37116  dochsat0  37184  lcfl6  37227  rp-fakeimass  37736
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 185  df-or 370
  Copyright terms: Public domain W3C validator