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  1664  axi12  2436  axbnd  2437  sspss  3596  pwpw0  4168  sssn  4178  pwsnALT  4233  unissint  4299  disjxiun  4437  pwssun  4779  ordtr3  4916  ordtri2or  4966  unizlim  4987  fvclss  6133  orduniorsuc  6636  ordzsl  6651  nn0suc  6695  xpexr  6714  odi  7218  swoso  7332  erdisj  7349  ordtypelem7  7938  wemapsolem  7964  domwdom  7989  iscard3  8463  ackbij1lem18  8606  fin56  8762  entric  8921  gchdomtri  8996  inttsk  9141  r1tskina  9149  psslinpr  9398  ssxr  9643  letric  9674  mul0or  10178  mulge0b  10401  zeo  10935  uzm1  11101  xrletri  11346  supxrgtmnf  11510  fzm1  11747  sq01  12243  ruclem3  13816  phiprmpw  14154  pleval2i  15440  irredn0  17129  drngmul0or  17193  lvecvs0or  17530  lssvs0or  17532  lspsnat  17567  lsppratlem1  17569  domnchr  18329  fctop  19264  cctop  19266  ppttop  19267  clslp  19408  restntr  19442  cnconn  19682  txindis  19863  txcon  19918  isufil2  20137  ufprim  20138  alexsubALTlem3  20277  pmltpc  21590  iundisj2  21687  limcco  22025  fta1b  22298  aalioulem2  22456  abelthlem2  22554  logreclem  22871  dchrfi  23251  2sqb  23374  tgbtwnconn1  23682  legov3  23704  coltr  23733  colline  23736  tglowdim2ln  23738  ragperp  23795  lmieu  23820  lmicom  23824  lmimid  23829  nvmul0or  25073  hvmul0or  25468  atomli  26827  atordi  26829  iundisj2f  26972  iundisj2fi  27120  signsply0  27998  cvmsdisj  28205  nepss  28420  dfon2lem6  28647  soseq  28761  btwnconn1lem13  29176  wl-exeq  29414  pm10.57  30673  icccncfext  31045  lsator0sp  33673  lkreqN  33842  2at0mat0  34196  trlator0  34842  dochkrshp4  36061  dochsat0  36129  lcfl6  36172