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

Theorem orrd 368
Description: Deduce implication from disjunction. (Contributed by NM, 27-Nov-1995.)
Hypothesis
Ref Expression
orrd.1  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Assertion
Ref Expression
orrd  |-  ( ph  ->  ( ps  \/  ch ) )

Proof of Theorem orrd
StepHypRef Expression
1 orrd.1 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
2 pm2.54 364 . 2  |-  ( ( -.  ps  ->  ch )  ->  ( ps  \/  ch ) )
31, 2syl 16 1  |-  ( ph  ->  ( ps  \/  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358
This theorem is referenced by:  olc  374  orc  375  pm2.68  400  pm4.79  567  axi12  2415  axbnd  2416  sspss  3446  pwpw0  3946  sssn  3957  pwsnALT  4010  unissint  4074  disjxiun  4209  pwssun  4489  ordtr3  4626  ordtri2or  4677  unizlim  4698  orduniorsuc  4810  ordzsl  4825  nn0suc  4869  xpexr  5307  fvclss  5980  odi  6822  swoso  6936  erdisj  6952  ordtypelem7  7493  wemapso2lem  7519  domwdom  7542  iscard3  7974  ackbij1lem18  8117  fin56  8273  entric  8432  gchdomtri  8504  inttsk  8649  r1tskina  8657  psslinpr  8908  ssxr  9145  letric  9174  mul0or  9662  zeo  10355  uzm1  10516  xrletri  10744  supxrgtmnf  10908  fzm1  11127  sq01  11501  ruclem3  12832  phiprmpw  13165  pleval2i  14421  irredn0  15808  drngmul0or  15856  lvecvs0or  16180  lssvs0or  16182  lspsnat  16217  lsppratlem1  16219  domnchr  16813  fctop  17068  cctop  17070  ppttop  17071  clslp  17212  restntr  17246  cnconn  17485  txindis  17666  txcon  17721  isufil2  17940  ufprim  17941  alexsubALTlem3  18080  pmltpc  19347  iundisj2  19443  limcco  19780  fta1b  20092  aalioulem2  20250  abelthlem2  20348  logreclem  20660  dchrfi  21039  2sqb  21162  nvmul0or  22133  hvmul0or  22527  atomli  23885  atordi  23887  iundisj2f  24030  iundisj2fi  24153  cvmsdisj  24957  nepss  25175  mulge0b  25191  dfon2lem6  25415  soseq  25529  btwnconn1lem13  26033  wl-exeq  26234  pm10.57  27543  lsator0sp  29799  lkreqN  29968  2at0mat0  30322  trlator0  30968  dochkrshp4  32187  dochsat0  32255  lcfl6  32298
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator