Theorem orrd 384

Description: Deduce disjunction from implication. (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

Step	Hyp	Ref	Expression
1		orrd.1	. 2 |- ( ph -> ( -. ps -> ch ) )
2		pm2.54 380	. 2 |- ( ( -. ps -> ch ) -> ( ps \/ ch ) )
3	1, 2	syl 17	1 |- ( ph -> ( ps \/ ch ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 374

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 190  df-or 376

This theorem is referenced by:  olc  390  orc  391  pm2.68  416  pm4.79  591  19.30  1754  axi12  2439  axbnd  2440  sspss  3543  pwpw0  4132  sssn  4142  pwsnALT  4206  unissint  4272  disjxiun  4412  pwssun  4758  ordtr3  5486  ordtri2or  5536  unizlim  5557  fvclss  6171  orduniorsuc  6683  ordzsl  6698  nn0suc  6743  xpexr  6759  odi  7305  swoso  7419  erdisj  7436  ordtypelem7  8064  wemapsolem  8090  domwdom  8114  iscard3  8549  ackbij1lem18  8692  fin56  8848  entric  9007  gchdomtri  9079  inttsk  9224  r1tskina  9232  psslinpr  9481  ssxr  9728  letric  9759  mul0or  10279  mulge0b  10502  zeo  11049  uzm1  11217  xrletri  11478  supxrgtmnf  11643  sq01  12425  ruclem3  14333  phiprmpw  14772  pleval2i  16258  irredn0  17979  drngmul0or  18044  lvecvs0or  18379  lssvs0or  18381  lspsnat  18416  lsppratlem1  18418  domnchr  19151  fctop  20067  cctop  20069  ppttop  20070  clslp  20212  restntr  20246  cnconn  20485  txindis  20697  txcon  20752  isufil2  20971  ufprim  20972  alexsubALTlem3  21112  pmltpc  22449  iundisj2  22550  limcco  22896  fta1b  23168  aalioulem2  23337  abelthlem2  23435  logreclem  23747  dchrfi  24231  2sqb  24354  tgbtwnconn1  24668  legov3  24691  coltr  24740  colline  24742  tglowdim2ln  24744  ragflat3  24799  ragperp  24810  lmieu  24874  lmicom  24878  lmimid  24884  nvmul0or  26321  hvmul0or  26726  atomli  28083  atordi  28085  iundisj2f  28248  iundisj2fi  28421  signsply0  29488  cvmsdisj  30041  nepss  30398  dfon2lem6  30482  soseq  30540  btwnconn1lem13  30914  wl-exeq  31911  lsator0sp  32611  lkreqN  32780  2at0mat0  33134  trlator0  33781  dochkrshp4  35001  dochsat0  35069  lcfl6  35112  rp-fakeimass  36200  frege124d  36397  pm10.57  36763  icccncfext  37802  fourierdlem70  38077  uzlidlring  40201  nneop  40605