Theorem ord 383

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 376	. 2 |- ( ( ps \/ ch ) <-> ( -. ps -> ch ) )
3	1, 2	sylib 201	1 |- ( ph -> ( -. ps -> ch ) )

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

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 190  df-or 376

This theorem is referenced by:  ornld  914  orcanai  929  oplem1  981  ecase23d  1383  19.33b  1758  elpwunsn  4023  eqsn  4145  disji2  4402  disjxiun  4412  pwssun  4758  swopo  4783  somo  4807  frsn  4923  ordtri3or  5473  ordtri1  5474  ordtri3  5477  ord0eln0  5495  suc11  5544  foconst  5826  ordeleqon  6641  ssonprc  6645  onmindif2  6665  limsssuc  6703  limom  6733  onfununi  7085  oeeulem  7327  uniinqs  7468  pw2f1olem  7701  pssnn  7815  ordtypelem9  8066  ordtypelem10  8067  oismo  8080  preleq  8147  suc11reg  8149  cantnfp1lem2  8209  cantnflem1  8219  cnfcom2lem  8231  cnfcom3lem  8233  rankxpsuc  8378  cardlim  8431  alephdom  8537  cardaleph  8545  iscard3  8549  pwcdadom  8671  cfslbn  8722  fin1a2lem12  8866  gchi  9074  fpwwe2lem13  9092  tskssel  9207  inttsk  9224  inar1  9225  r1tskina  9232  tskuni  9233  gruina  9268  grur1  9270  nlt1pi  9356  nqereu  9379  leltne  9748  nneo  11047  zeo2  11050  xrleltne  11472  nltpnft  11489  ngtmnft  11490  xrrebnd  11491  xaddf  11545  xrsupsslem  11620  xrinfmsslem  11621  fzocatel  12008  seqf1olem1  12283  seqf1olem2  12284  discr1  12439  hashnncl  12578  seqcoll2  12660  sqeqd  13277  sqrmo  13363  isercoll  13779  dvdseq  14400  bitsfzo  14457  bitsinv1lem  14463  bitsf1  14468  bezoutlem3OLD  14553  bezoutlem3  14556  eucalglt  14592  phibndlem  14766  dfphi2  14770  prmdiv  14781  odzdvds  14788  odzdvdsOLD  14794  pceq0  14868  pc2dvds  14876  fldivp1  14890  pcfac  14892  prmreclem3  14910  1arith  14919  4sqlem10  14939  4sqlem17OLD  14953  4sqlem18OLD  14954  4sqlem17  14959  4sqlem18  14960  vdwlem6  14984  ramubcl  15024  ramcl  15035  mrissmrcd  15594  psgnunilem5  17183  oddvdsnn0  17241  odnncl  17242  oddvds  17244  odcl2  17264  gexdvds  17283  gexnnod  17288  sylow1lem1  17298  odcau  17304  pgpssslw  17314  efgs1b  17434  efgredlema  17438  torsubg  17540  prmcyg  17576  gsumval3eu  17586  ablfacrplem  17746  ablfac1eu  17754  lspdisj  18396  lspsncv0  18417  fidomndrnglem  18578  gzrngunitlem  19080  prmirredlem  19112  fctop  20067  cctop  20069  ppttop  20070  pptbas  20071  ordtrest2lem  20267  conclo  20478  txindis  20697  filcon  20946  ufilb  20969  cldsubg  21173  reconnlem1  21892  reconnlem2  21893  metds0  21915  metdseq0  21919  metnrmlem1a  21923  metds0OLD  21930  metdseq0OLD  21934  metnrmlem1aOLD  21938  iccpnfhmeo  22021  xrhmeo  22022  cphsubrglem  22203  minveclem3b  22418  minveclem4a  22420  minveclem3bOLD  22430  minveclem4aOLD  22432  vitalilem4  22617  itg2gt0  22766  itgsplitioo  22843  limccnp2  22895  rollelem  22989  dvlip  22993  itgsubstlem  23048  plyaddlem1  23215  plymullem1  23216  coefv0  23250  dgreq0  23267  radcnv0  23419  pserdvlem2  23431  pilem2  23455  pilem2OLD  23456  sineq0  23524  logtayl  23653  cxpsqrt  23696  isosctrlem2  23796  atantayl2  23912  leibpilem1  23914  rlimcnp2  23940  amgm  23964  basellem3  24057  muval2  24109  sqf11  24114  ppinprm  24127  chtnprm  24129  perfectlem2  24206  lgsdir  24306  lgsabs1  24310  lgseisenlem1  24325  2sqlem7  24346  2sqblem  24353  chebbnd1lem1  24355  dchrisum0flblem1  24394  pntpbnd1  24472  pntpbnd2  24473  ostth  24525  symquadlem  24782  midexlem  24785  colperp  24819  midex  24827  oppperpex  24843  outpasch  24845  hlpasch  24846  hpgerlem  24855  colopp  24859  colhp  24860  lmieu  24874  lmicom  24878  trgcopy  24894  cgracol  24917  minvecolem5  26571  minvecolem5OLD  26581  staddi  27947  stadd3i  27949  atsseq  28048  atom1d  28054  atoml2i  28084  disji2f  28235  disjif2  28239  znsqcld  28371  2sqmod  28457  psgnfzto1stlem  28661  ordtrest2NEWlem  28776  eulerpartlemb  29249  sgn3da  29460  subfacp1lem6  29956  cvmscld  30044  cvmsss2  30045  cvmseu  30047  nosepon  30604  ordtoplem  31143  ordcmp  31155  poimirlem25  32009  heiborlem6  32192  isfldidl  32345  pridlc2  32349  mpt2bi123f  32450  mptbi12f  32454  ac6s6  32459  lsatcmp  32613  lsatcmp2  32614  2atm  33136  trlatn0  33782  trlval3  33797  cdleme18c  33903  cdlemg17b  34273  cdlemg17i  34280  cdlemh  34428  dia2dimlem2  34677  dia2dimlem3  34678  dochlkr  34997  dochkrshp  34998  lcfl6  35112  lcfrlem9  35162  hdmap14lem6  35488  hgmapval0  35507  ctbnfien  35705  pw2f1ocnv  35936  unxpwdom3  35997  dgrsub2  36038  rp-fakeanorass  36201  disjxp1  37448  fmul01lt1lem1  37699  elprn1  37750  stoweidlem35  37933  stirlinglem5  37977  stirlinglem12  37984  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem93  38100  perfectALTVlem2  38881