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

Theorem orrd 367
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 363 . 2  |-  ( ( -.  ps  ->  ch )  ->  ( ps  \/  ch ) )
31, 2syl 15 1  |-  ( ph  ->  ( ps  \/  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357
This theorem is referenced by:  olc  373  orc  374  pm2.68  399  pm4.79  566  sspss  3275  pwpw0  3763  sssn  3772  pwsnALT  3822  unissint  3886  disjxiun  4020  pwssun  4299  ordtr3  4437  ordtri2or  4488  unizlim  4509  orduniorsuc  4621  ordzsl  4636  nn0suc  4680  xpexr  5114  fvclss  5760  odi  6577  swoso  6691  erdisj  6707  ordtypelem7  7239  wemapso2lem  7265  domwdom  7288  iscard3  7720  ackbij1lem18  7863  fin56  8019  entric  8179  gchdomtri  8251  inttsk  8396  r1tskina  8404  psslinpr  8655  ssxr  8892  letric  8921  mul0or  9408  zeo  10097  uzm1  10258  xrletri  10485  supxrgtmnf  10648  fzm1  10862  sq01  11223  ruclem3  12511  phiprmpw  12844  pleval2i  14098  irredn0  15485  drngmul0or  15533  lvecvs0or  15861  lssvs0or  15863  lspsnat  15898  lsppratlem1  15900  domnchr  16486  fctop  16741  cctop  16743  ppttop  16744  clslp  16879  restntr  16912  cnconn  17148  txindis  17328  txcon  17383  isufil2  17603  ufprim  17604  alexsubALTlem3  17743  pmltpc  18810  iundisj2  18906  limcco  19243  fta1b  19555  aalioulem2  19713  abelthlem2  19808  logreclem  20116  dchrfi  20494  2sqb  20617  nvmul0or  21210  hvmul0or  21604  atomli  22962  atordi  22964  iundisj2fi  23364  iundisj2f  23366  cvmsdisj  23801  nepss  24072  mulge0b  24086  dfon2lem6  24144  soseq  24254  btwnconn1lem13  24722  nxtor  24985  fixpc  25094  pm10.57  27566  stoweidlem34  27783  lsator0sp  29191  lkreqN  29360  2at0mat0  29714  trlator0  30360  dochkrshp4  31579  dochsat0  31647  lcfl6  31690
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 177  df-or 359
  Copyright terms: Public domain W3C validator