Theorem orrd 378

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 374	. 2 |- ( ( -. ps -> ch ) -> ( ps \/ ch ) )
3	1, 2	syl 16	1 |- ( ph -> ( ps \/ ch ) )

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

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 185  df-or 370

This theorem is referenced by:  olc  384  orc  385  pm2.68  410  pm4.79  583  19.30  1677  axi12  2417  axbnd  2418  sspss  3585  pwpw0  4159  sssn  4169  pwsnALT  4225  unissint  4292  disjxiun  4430  pwssun  4772  ordtr3  4909  ordtri2or  4959  unizlim  4980  fvclss  6135  orduniorsuc  6646  ordzsl  6661  nn0suc  6705  xpexr  6721  odi  7226  swoso  7340  erdisj  7357  ordtypelem7  7947  wemapsolem  7973  domwdom  7998  iscard3  8472  ackbij1lem18  8615  fin56  8771  entric  8930  gchdomtri  9005  inttsk  9150  r1tskina  9158  psslinpr  9407  ssxr  9652  letric  9683  mul0or  10190  mulge0b  10413  zeo  10949  uzm1  11115  xrletri  11361  supxrgtmnf  11525  fzm1  11762  sq01  12262  ruclem3  13838  phiprmpw  14178  pleval2i  15463  irredn0  17220  drngmul0or  17285  lvecvs0or  17622  lssvs0or  17624  lspsnat  17659  lsppratlem1  17661  domnchr  18436  fctop  19371  cctop  19373  ppttop  19374  clslp  19515  restntr  19549  cnconn  19789  txindis  20001  txcon  20056  isufil2  20275  ufprim  20276  alexsubALTlem3  20415  pmltpc  21728  iundisj2  21825  limcco  22163  fta1b  22436  aalioulem2  22594  abelthlem2  22692  logreclem  23015  dchrfi  23395  2sqb  23518  tgbtwnconn1  23827  legov3  23849  coltr  23892  colline  23895  tglowdim2ln  23897  ragflat3  23948  ragperp  23959  lmieu  24015  lmicom  24019  lmimid  24024  nvmul0or  25412  hvmul0or  25807  atomli  27166  atordi  27168  iundisj2f  27314  iundisj2fi  27467  signsply0  28374  cvmsdisj  28581  nepss  28961  dfon2lem6  29188  soseq  29302  btwnconn1lem13  29717  wl-exeq  29955  pm10.57  31223  icccncfext  31593  fourierdlem70  31844  uzlidlring  32435  lsator0sp  34428  lkreqN  34597  2at0mat0  34951  trlator0  35598  dochkrshp4  36818  dochsat0  36886  lcfl6  36929  rp-fakeimass  37401