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  1660  axi12  2428  axbnd  2429  sspss  3553  pwpw0  4119  sssn  4129  pwsnALT  4184  unissint  4250  disjxiun  4387  pwssun  4725  ordtr3  4862  ordtri2or  4912  unizlim  4933  fvclss  6058  orduniorsuc  6541  ordzsl  6556  nn0suc  6600  xpexr  6618  odi  7118  swoso  7232  erdisj  7248  ordtypelem7  7839  wemapsolem  7865  domwdom  7890  iscard3  8364  ackbij1lem18  8507  fin56  8663  entric  8822  gchdomtri  8897  inttsk  9042  r1tskina  9050  psslinpr  9301  ssxr  9545  letric  9576  mul0or  10077  mulge0b  10300  zeo  10828  uzm1  10992  xrletri  11229  supxrgtmnf  11393  fzm1  11641  sq01  12087  ruclem3  13617  phiprmpw  13953  pleval2i  15236  irredn0  16901  drngmul0or  16959  lvecvs0or  17295  lssvs0or  17297  lspsnat  17332  lsppratlem1  17334  domnchr  18072  fctop  18724  cctop  18726  ppttop  18727  clslp  18868  restntr  18902  cnconn  19142  txindis  19323  txcon  19378  isufil2  19597  ufprim  19598  alexsubALTlem3  19737  pmltpc  21050  iundisj2  21146  limcco  21484  fta1b  21757  aalioulem2  21915  abelthlem2  22013  logreclem  22330  dchrfi  22710  2sqb  22833  tgbtwnconn1  23127  coltr  23174  colline  23177  tglowdim2ln  23179  ragperp  23236  nvmul0or  24167  hvmul0or  24562  atomli  25921  atordi  25923  iundisj2f  26066  iundisj2fi  26215  signsply0  27086  cvmsdisj  27293  nepss  27508  dfon2lem6  27735  soseq  27849  btwnconn1lem13  28264  wl-exeq  28501  pm10.57  29761  lsator0sp  32952  lkreqN  33121  2at0mat0  33475  trlator0  34121  dochkrshp4  35340  dochsat0  35408  lcfl6  35451