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  1659  axi12  2417  axbnd  2418  sspss  3450  pwpw0  4016  sssn  4026  pwsnALT  4081  unissint  4147  disjxiun  4284  pwssun  4622  ordtr3  4759  ordtri2or  4809  unizlim  4830  fvclss  5954  orduniorsuc  6436  ordzsl  6451  nn0suc  6495  xpexr  6513  odi  7010  swoso  7124  erdisj  7140  ordtypelem7  7730  wemapsolem  7756  domwdom  7781  iscard3  8255  ackbij1lem18  8398  fin56  8554  entric  8713  gchdomtri  8788  inttsk  8933  r1tskina  8941  psslinpr  9192  ssxr  9436  letric  9467  mul0or  9968  mulge0b  10191  zeo  10719  uzm1  10883  xrletri  11120  supxrgtmnf  11284  fzm1  11532  sq01  11978  ruclem3  13507  phiprmpw  13843  pleval2i  15126  irredn0  16785  drngmul0or  16833  lvecvs0or  17169  lssvs0or  17171  lspsnat  17206  lsppratlem1  17208  domnchr  17943  fctop  18588  cctop  18590  ppttop  18591  clslp  18732  restntr  18766  cnconn  19006  txindis  19187  txcon  19242  isufil2  19461  ufprim  19462  alexsubALTlem3  19601  pmltpc  20914  iundisj2  21010  limcco  21348  fta1b  21621  aalioulem2  21779  abelthlem2  21877  logreclem  22194  dchrfi  22574  2sqb  22697  tgbtwnconn1  22987  colline  23032  nvmul0or  24000  hvmul0or  24395  atomli  25754  atordi  25756  iundisj2f  25900  iundisj2fi  26049  signsply0  26921  cvmsdisj  27128  nepss  27343  dfon2lem6  27570  soseq  27684  btwnconn1lem13  28099  wl-exeq  28332  pm10.57  29594  lsator0sp  32539  lkreqN  32708  2at0mat0  33062  trlator0  33708  dochkrshp4  34927  dochsat0  34995  lcfl6  35038