Theorem ord 377

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 370	. 2 |- ( ( ps \/ ch ) <-> ( -. ps -> ch ) )
3	1, 2	sylib 196	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:  ornld  898  orcanai  913  oplem1  964  ecase23d  1332  19.33b  1697  elpwunsn  4073  eqsn  4193  disji2  4443  disjxiun  4453  pwssun  4795  swopo  4819  somo  4843  ordtri3or  4919  ordtri1  4920  ordtri3  4923  ord0eln0  4941  suc11  4990  frsn  5079  foconst  5812  ordeleqon  6623  ssonprc  6626  onmindif2  6646  limsssuc  6684  limom  6714  onfununi  7030  oeeulem  7268  uniinqs  7409  pw2f1olem  7640  pssnn  7757  ordtypelem9  7969  ordtypelem10  7970  oismo  7983  preleq  8051  suc11reg  8053  cantnfp1lem2  8115  cantnflem1  8125  cantnfp1lem2OLD  8141  cantnflem1OLD  8148  cnfcom2lem  8162  cnfcom3lem  8164  cnfcom2lemOLD  8170  cnfcom3lemOLD  8172  rankxpsuc  8317  cardlim  8370  alephdom  8479  cardaleph  8487  iscard3  8491  pwcdadom  8613  cfslbn  8664  fin1a2lem12  8808  gchi  9019  fpwwe2lem13  9037  tskssel  9152  inttsk  9169  inar1  9170  r1tskina  9177  tskuni  9178  gruina  9213  grur1  9215  nlt1pi  9301  nqereu  9324  leltne  9691  nneo  10967  zeo2  10970  xrleltne  11376  nltpnft  11392  ngtmnft  11393  xrrebnd  11394  xaddf  11448  xrsupsslem  11523  xrinfmsslem  11524  fzocatel  11883  seqf1olem1  12149  seqf1olem2  12150  discr1  12305  hashnncl  12439  seqcoll2  12517  sqeqd  13011  sqrmo  13097  isercoll  13502  dvdseq  14045  bitsfzo  14097  bitsinv1lem  14103  bitsf1  14108  bezoutlem3  14190  eucalglt  14226  phibndlem  14312  dfphi2  14316  prmdiv  14327  odzdvds  14334  pceq0  14406  pc2dvds  14414  fldivp1  14428  pcfac  14430  prmreclem3  14448  1arith  14457  4sqlem10  14477  4sqlem17  14491  4sqlem18  14492  vdwlem6  14516  ramubcl  14548  ramcl  14559  mrissmrcd  15057  psgnunilem5  16646  oddvdsnn0  16695  odnncl  16696  oddvds  16698  odcl2  16714  gexdvds  16731  gexnnod  16735  sylow1lem1  16745  odcau  16751  pgpssslw  16761  efgs1b  16881  efgredlema  16885  torsubg  16987  prmcyg  17023  gsumval3eu  17034  ablfacrplem  17243  ablfac1eu  17251  lspdisj  17898  lspsncv0  17919  fidomndrnglem  18082  gzrngunitlem  18609  prmirredlem  18650  prmirredlemOLD  18653  fctop  19632  cctop  19634  ppttop  19635  pptbas  19636  ordtrest2lem  19831  conclo  20042  txindis  20261  filcon  20510  ufilb  20533  cldsubg  20735  reconnlem1  21457  reconnlem2  21458  metds0  21480  metdseq0  21484  metnrmlem1a  21488  iccpnfhmeo  21571  xrhmeo  21572  cphsubrglem  21750  minveclem3b  21969  minveclem4a  21971  vitalilem4  22146  itg2gt0  22293  itgsplitioo  22370  limccnp2  22422  rollelem  22516  dvlip  22520  itgsubstlem  22575  plyaddlem1  22736  plymullem1  22737  coefv0  22771  dgreq0  22788  radcnv0  22937  pserdvlem2  22949  pilem2  22973  sineq0  23040  logtayl  23167  cxpsqrt  23210  isosctrlem2  23279  atantayl2  23395  leibpilem1  23397  rlimcnp2  23422  amgm  23446  basellem3  23482  muval2  23534  sqf11  23539  ppinprm  23552  chtnprm  23554  perfectlem2  23631  lgsdir  23731  lgsabs1  23735  lgseisenlem1  23750  2sqlem7  23771  2sqblem  23778  chebbnd1lem1  23780  dchrisum0flblem1  23819  pntpbnd1  23897  pntpbnd2  23898  ostth  23950  coltr2  24154  symquadlem  24192  midexlem  24195  colperp  24229  midex  24237  hpgerlem  24260  lmieu  24276  lmicom  24280  minvecolem5  25924  staddi  27292  stadd3i  27294  atsseq  27393  atom1d  27399  atoml2i  27429  disji2f  27577  disjif2  27581  znsqcld  27718  2sqmod  27796  ordtrest2NEWlem  28065  eulerpartlemb  28504  sgn3da  28677  subfacp1lem6  28826  cvmscld  28915  cvmsss2  28916  cvmseu  28918  ordtoplem  30105  ordcmp  30117  heiborlem6  30517  isfldidl  30670  pridlc2  30674  mpt2bi123f  30776  mptbi12f  30780  ac6s6  30785  ctbnfien  30956  pw2f1ocnv  31183  unxpwdom3  31245  dgrsub2  31288  fmul01lt1lem1  31781  elprn1  31842  stoweidlem35  32020  stirlinglem5  32063  stirlinglem12  32070  fourierdlem42  32134  fourierdlem93  32185  lsatcmp  34871  lsatcmp2  34872  2atm  35394  trlatn0  36040  trlval3  36055  cdleme18c  36161  cdlemg17b  36531  cdlemg17i  36538  cdlemh  36686  dia2dimlem2  36935  dia2dimlem3  36936  dochlkr  37255  dochkrshp  37256  lcfl6  37370  lcfrlem9  37420  hdmap14lem6  37746  hgmapval0  37765  rp-fakeanorass  37897