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  3288  pwpw0  3779  sssn  3788  pwsnALT  3838  unissint  3902  disjxiun  4036  pwssun  4315  ordtr3  4453  ordtri2or  4504  unizlim  4525  orduniorsuc  4637  ordzsl  4652  nn0suc  4696  xpexr  5130  fvclss  5776  odi  6593  swoso  6707  erdisj  6723  ordtypelem7  7255  wemapso2lem  7281  domwdom  7304  iscard3  7736  ackbij1lem18  7879  fin56  8035  entric  8195  gchdomtri  8267  inttsk  8412  r1tskina  8420  psslinpr  8671  ssxr  8908  letric  8937  mul0or  9424  zeo  10113  uzm1  10274  xrletri  10501  supxrgtmnf  10664  fzm1  10878  sq01  11239  ruclem3  12527  phiprmpw  12860  pleval2i  14114  irredn0  15501  drngmul0or  15549  lvecvs0or  15877  lssvs0or  15879  lspsnat  15914  lsppratlem1  15916  domnchr  16502  fctop  16757  cctop  16759  ppttop  16760  clslp  16895  restntr  16928  cnconn  17164  txindis  17344  txcon  17399  isufil2  17619  ufprim  17620  alexsubALTlem3  17759  pmltpc  18826  iundisj2  18922  limcco  19259  fta1b  19571  aalioulem2  19729  abelthlem2  19824  logreclem  20132  dchrfi  20510  2sqb  20633  nvmul0or  21226  hvmul0or  21620  atomli  22978  atordi  22980  iundisj2fi  23379  iundisj2f  23381  cvmsdisj  23816  nepss  24087  mulge0b  24101  dfon2lem6  24215  soseq  24325  btwnconn1lem13  24794  nxtor  25088  fixpc  25197  pm10.57  27669  stoweidlem34  27886  lsator0sp  29813  lkreqN  29982  2at0mat0  30336  trlator0  30982  dochkrshp4  32201  dochsat0  32269  lcfl6  32312
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