MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orrd 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  2383  axbnd  2384  sspss  3406  pwpw0  3906  sssn  3917  pwsnALT  3970  unissint  4034  disjxiun  4169  pwssun  4449  ordtr3  4586  ordtri2or  4636  unizlim  4657  orduniorsuc  4769  ordzsl  4784  nn0suc  4828  xpexr  5266  fvclss  5939  odi  6781  swoso  6895  erdisj  6911  ordtypelem7  7449  wemapso2lem  7475  domwdom  7498  iscard3  7930  ackbij1lem18  8073  fin56  8229  entric  8388  gchdomtri  8460  inttsk  8605  r1tskina  8613  psslinpr  8864  ssxr  9101  letric  9130  mul0or  9618  zeo  10311  uzm1  10472  xrletri  10700  supxrgtmnf  10864  fzm1  11082  sq01  11456  ruclem3  12787  phiprmpw  13120  pleval2i  14376  irredn0  15763  drngmul0or  15811  lvecvs0or  16135  lssvs0or  16137  lspsnat  16172  lsppratlem1  16174  domnchr  16768  fctop  17023  cctop  17025  ppttop  17026  clslp  17166  restntr  17200  cnconn  17438  txindis  17619  txcon  17674  isufil2  17893  ufprim  17894  alexsubALTlem3  18033  pmltpc  19300  iundisj2  19396  limcco  19733  fta1b  20045  aalioulem2  20203  abelthlem2  20301  logreclem  20613  dchrfi  20992  2sqb  21115  nvmul0or  22086  hvmul0or  22480  atomli  23838  atordi  23840  iundisj2f  23983  iundisj2fi  24106  cvmsdisj  24910  nepss  25128  mulge0b  25144  dfon2lem6  25358  soseq  25468  btwnconn1lem13  25937  pm10.57  27434  lsator0sp  29484  lkreqN  29653  2at0mat0  30007  trlator0  30653  dochkrshp4  31872  dochsat0  31940  lcfl6  31983
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