Theorem ord 379

Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)

Hypothesis

Ref	Expression
ord.1	|- ( ph -> ( ps \/ ch ) )

Assertion

Ref	Expression
ord	|- ( ph -> ( -. ps -> ch ) )

Proof of Theorem ord

Step	Hyp	Ref	Expression
1		ord.1	. 2 |- ( ph -> ( ps \/ ch ) )
2		df-or 372	. 2 |- ( ( ps \/ ch ) <-> ( -. ps -> ch ) )
3	1, 2	sylib 200	1 |- ( ph -> ( -. ps -> ch ) )

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

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 189  df-or 372

This theorem is referenced by:  ornld  907  orcanai  922  oplem1  973  ecase23d  1369  19.33b  1741  elpwunsn  4038  eqsn  4159  disji2  4408  disjxiun  4418  pwssun  4757  swopo  4782  somo  4806  frsn  4922  ordtri3or  5472  ordtri1  5473  ordtri3  5476  ord0eln0  5494  suc11  5543  foconst  5819  ordeleqon  6627  ssonprc  6631  onmindif2  6651  limsssuc  6689  limom  6719  onfununi  7066  oeeulem  7308  uniinqs  7449  pw2f1olem  7680  pssnn  7794  ordtypelem9  8045  ordtypelem10  8046  oismo  8059  preleq  8126  suc11reg  8128  cantnfp1lem2  8187  cantnflem1  8197  cnfcom2lem  8209  cnfcom3lem  8211  rankxpsuc  8356  cardlim  8409  alephdom  8514  cardaleph  8522  iscard3  8526  pwcdadom  8648  cfslbn  8699  fin1a2lem12  8843  gchi  9051  fpwwe2lem13  9069  tskssel  9184  inttsk  9201  inar1  9202  r1tskina  9209  tskuni  9210  gruina  9245  grur1  9247  nlt1pi  9333  nqereu  9356  leltne  9725  nneo  11021  zeo2  11024  xrleltne  11446  nltpnft  11463  ngtmnft  11464  xrrebnd  11465  xaddf  11519  xrsupsslem  11594  xrinfmsslem  11595  fzocatel  11979  seqf1olem1  12253  seqf1olem2  12254  discr1  12409  hashnncl  12548  seqcoll2  12627  sqeqd  13223  sqrmo  13309  isercoll  13724  dvdseq  14345  bitsfzo  14402  bitsinv1lem  14408  bitsf1  14413  bezoutlem3OLD  14498  bezoutlem3  14501  eucalglt  14537  phibndlem  14711  dfphi2  14715  prmdiv  14726  odzdvds  14733  odzdvdsOLD  14739  pceq0  14813  pc2dvds  14821  fldivp1  14835  pcfac  14837  prmreclem3  14855  1arith  14864  4sqlem10  14884  4sqlem17OLD  14898  4sqlem18OLD  14899  4sqlem17  14904  4sqlem18  14905  vdwlem6  14929  ramubcl  14969  ramcl  14980  mrissmrcd  15539  psgnunilem5  17128  oddvdsnn0  17186  odnncl  17187  oddvds  17189  odcl2  17209  gexdvds  17228  gexnnod  17233  sylow1lem1  17243  odcau  17249  pgpssslw  17259  efgs1b  17379  efgredlema  17383  torsubg  17485  prmcyg  17521  gsumval3eu  17531  ablfacrplem  17691  ablfac1eu  17699  lspdisj  18341  lspsncv0  18362  fidomndrnglem  18523  gzrngunitlem  19025  prmirredlem  19056  fctop  20011  cctop  20013  ppttop  20014  pptbas  20015  ordtrest2lem  20211  conclo  20422  txindis  20641  filcon  20890  ufilb  20913  cldsubg  21117  reconnlem1  21836  reconnlem2  21837  metds0  21859  metdseq0  21863  metnrmlem1a  21867  metds0OLD  21874  metdseq0OLD  21878  metnrmlem1aOLD  21882  iccpnfhmeo  21965  xrhmeo  21966  cphsubrglem  22147  minveclem3b  22362  minveclem4a  22364  minveclem3bOLD  22374  minveclem4aOLD  22376  vitalilem4  22561  itg2gt0  22710  itgsplitioo  22787  limccnp2  22839  rollelem  22933  dvlip  22937  itgsubstlem  22992  plyaddlem1  23159  plymullem1  23160  coefv0  23194  dgreq0  23211  radcnv0  23363  pserdvlem2  23375  pilem2  23399  pilem2OLD  23400  sineq0  23468  logtayl  23597  cxpsqrt  23640  isosctrlem2  23740  atantayl2  23856  leibpilem1  23858  rlimcnp2  23884  amgm  23908  basellem3  24001  muval2  24053  sqf11  24058  ppinprm  24071  chtnprm  24073  perfectlem2  24150  lgsdir  24250  lgsabs1  24254  lgseisenlem1  24269  2sqlem7  24290  2sqblem  24297  chebbnd1lem1  24299  dchrisum0flblem1  24338  pntpbnd1  24416  pntpbnd2  24417  ostth  24469  symquadlem  24726  midexlem  24729  colperp  24763  midex  24771  oppperpex  24787  outpasch  24789  hlpasch  24790  hpgerlem  24799  colopp  24803  colhp  24804  lmieu  24818  lmicom  24822  trgcopy  24838  cgracol  24861  minvecolem5  26515  minvecolem5OLD  26525  staddi  27891  stadd3i  27893  atsseq  27992  atom1d  27998  atoml2i  28028  disji2f  28183  disjif2  28187  znsqcld  28323  2sqmod  28410  psgnfzto1stlem  28615  ordtrest2NEWlem  28730  eulerpartlemb  29203  sgn3da  29414  subfacp1lem6  29910  cvmscld  29998  cvmsss2  29999  cvmseu  30001  ordtoplem  31094  ordcmp  31106  poimirlem25  31885  heiborlem6  32068  isfldidl  32221  pridlc2  32225  mpt2bi123f  32326  mptbi12f  32330  ac6s6  32335  lsatcmp  32494  lsatcmp2  32495  2atm  33017  trlatn0  33663  trlval3  33678  cdleme18c  33784  cdlemg17b  34154  cdlemg17i  34161  cdlemh  34309  dia2dimlem2  34558  dia2dimlem3  34559  dochlkr  34878  dochkrshp  34879  lcfl6  34993  lcfrlem9  35043  hdmap14lem6  35369  hgmapval0  35388  ctbnfien  35586  pw2f1ocnv  35818  unxpwdom3  35879  dgrsub2  35920  rp-fakeanorass  36083  disjxp1  37280  fmul01lt1lem1  37488  elprn1  37539  stoweidlem35  37722  stirlinglem5  37766  stirlinglem12  37773  fourierdlem42  37838  fourierdlem42OLD  37839  fourierdlem93  37889  perfectALTVlem2  38562