Theorem orrd 393

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

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

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 197  df-or 385

This theorem is referenced by:  olc  399  orc  400  pm2.68  426  pm4.79  607  19.30  1809  axi12  2600  axbnd  2601  sspss  3706  eqoreldif  4225  pwpw0  4344  sssn  4358  pwsnALT  4429  unissint  4501  disjiund  4643  disjxiun  4649  disjxiunOLD  4650  otsndisj  4979  otiunsndisj  4980  pwssun  5020  isso2i  5067  ordtr3  5769  ordtr3OLD  5770  ordtri2or  5822  unizlim  5844  fvclss  6500  orduniorsuc  7030  ordzsl  7045  nn0suc  7090  xpexr  7106  odi  7659  swoso  7775  erdisj  7794  ordtypelem7  8429  wemapsolem  8455  domwdom  8479  iscard3  8916  ackbij1lem18  9059  fin56  9215  entric  9379  gchdomtri  9451  inttsk  9596  r1tskina  9604  psslinpr  9853  ssxr  10107  letric  10137  mul0or  10667  mulge0b  10893  zeo  11463  uzm1  11718  xrletri  11984  supxrgtmnf  12159  sq01  12986  ruclem3  14962  prm2orodd  15404  phiprmpw  15481  pleval2i  16964  irredn0  18703  drngmul0or  18768  lvecvs0or  19108  lssvs0or  19110  lspsnat  19145  lsppratlem1  19147  domnchr  19880  fctop  20808  cctop  20810  ppttop  20811  clslp  20952  restntr  20986  cnconn  21225  txindis  21437  txconn  21492  isufil2  21712  ufprim  21713  alexsubALTlem3  21853  pmltpc  23219  iundisj2  23317  limcco  23657  fta1b  23929  aalioulem2  24088  abelthlem2  24186  logreclem  24500  dchrfi  24980  2sqb  25157  tgbtwnconn1  25470  legov3  25493  coltr  25542  colline  25544  tglowdim2ln  25546  ragflat3  25601  ragperp  25612  lmieu  25676  lmicom  25680  lmimid  25686  numedglnl  26039  nvmul0or  27505  hvmul0or  27882  atomli  29241  atordi  29243  iundisj2f  29403  iundisj2fi  29556  signsply0  30628  cvmsdisj  31252  nepss  31599  dfon2lem6  31693  soseq  31751  nosepdmlem  31833  noetalem3  31865  btwnconn1lem13  32206  wl-exeq  33321  lsator0sp  34288  lkreqN  34457  2at0mat0  34811  trlator0  35458  dochkrshp4  36678  dochsat0  36746  lcfl6  36789  rp-fakeimass  37857  frege124d  38053  clsk1independent  38344  pm10.57  38570  icccncfext  40100  fourierdlem70  40393  uzlidlring  41929  nneop  42320