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:  orcanai  904  oplem1  955  ecase23d  1322  19.33b  1663  elpwunsn  3938  eqsn  4055  disji2  4300  disjxiun  4310  pwssun  4648  swopo  4672  somo  4696  ordtri3or  4772  ordtri1  4773  ordtri3  4776  ord0eln0  4794  suc11  4843  frsn  4930  foconst  5652  ordeleqon  6421  ssonprc  6424  onmindif2  6444  limsssuc  6482  limom  6512  onfununi  6823  oeeulem  7061  uniinqs  7201  pw2f1olem  7436  pssnn  7552  ordtypelem9  7761  ordtypelem10  7762  oismo  7775  preleq  7844  suc11reg  7846  cantnfp1lem2  7908  cantnflem1  7918  cantnfp1lem2OLD  7934  cantnflem1OLD  7941  cnfcom2lem  7955  cnfcom3lem  7957  cnfcom2lemOLD  7963  cnfcom3lemOLD  7965  rankxpsuc  8110  cardlim  8163  alephdom  8272  cardaleph  8280  iscard3  8284  pwcdadom  8406  cfslbn  8457  fin1a2lem12  8601  gchi  8812  fpwwe2lem13  8830  tskssel  8945  inttsk  8962  inar1  8963  r1tskina  8970  tskuni  8971  gruina  9006  grur1  9008  nlt1pi  9096  nqereu  9119  leltne  9485  nneo  10746  zeo2  10749  xrleltne  11143  nltpnft  11159  ngtmnft  11160  xrrebnd  11161  xaddf  11215  xrsupsslem  11290  xrinfmsslem  11291  seqf1olem1  11866  seqf1olem2  11867  discr1  12021  hashnncl  12155  seqcoll2  12238  sqeqd  12676  sqrmo  12762  isercoll  13166  dvdseq  13601  bitsfzo  13652  bitsinv1lem  13658  bitsf1  13663  bezoutlem3  13745  eucalglt  13781  phibndlem  13866  dfphi2  13870  prmdiv  13881  odzdvds  13888  pceq0  13958  pc2dvds  13966  fldivp1  13980  pcfac  13982  prmreclem3  14000  1arith  14009  4sqlem10  14029  4sqlem17  14043  4sqlem18  14044  vdwlem6  14068  ramubcl  14100  ramcl  14111  mrissmrcd  14599  psgnunilem5  16021  oddvdsnn0  16068  odnncl  16069  oddvds  16071  odcl2  16087  gexdvds  16104  gexnnod  16108  sylow1lem1  16118  odcau  16124  pgpssslw  16134  efgs1b  16254  efgredlema  16258  torsubg  16357  prmcyg  16391  gsumval3eu  16402  ablfacrplem  16588  ablfac1eu  16596  lspdisj  17228  lspsncv0  17249  fidomndrnglem  17400  gzrngunitlem  17899  prmirredlem  17939  prmirredlemOLD  17942  fctop  18630  cctop  18632  ppttop  18633  pptbas  18634  ordtrest2lem  18829  conclo  19041  txindis  19229  filcon  19478  ufilb  19501  cldsubg  19703  reconnlem1  20425  reconnlem2  20426  metds0  20448  metdseq0  20452  metnrmlem1a  20456  iccpnfhmeo  20539  xrhmeo  20540  cphsubrglem  20718  minveclem3b  20937  minveclem4a  20939  vitalilem4  21113  itg2gt0  21260  itgsplitioo  21337  limccnp2  21389  rollelem  21483  dvlip  21487  itgsubstlem  21542  plyaddlem1  21703  plymullem1  21704  coefv0  21737  dgreq0  21754  radcnv0  21903  pserdvlem2  21915  pilem2  21939  sineq0  22005  logtayl  22127  cxpsqr  22170  isosctrlem2  22239  atantayl2  22355  leibpilem1  22357  rlimcnp2  22382  amgm  22406  basellem3  22442  muval2  22494  sqf11  22499  ppinprm  22512  chtnprm  22514  perfectlem2  22591  lgsdir  22691  lgsabs1  22695  lgseisenlem1  22710  2sqlem7  22731  2sqblem  22738  chebbnd1lem1  22740  dchrisum0flblem1  22779  pntpbnd1  22857  pntpbnd2  22858  ostth  22910  colmid  23104  symquadlem  23105  midexlem  23108  minvecolem5  24304  staddi  25672  stadd3i  25674  atsseq  25773  atom1d  25779  atoml2i  25809  disji2f  25943  disjif2  25947  ordtrest2NEWlem  26374  eulerpartlemb  26773  subfacp1lem6  27095  cvmscld  27184  cvmsss2  27185  cvmseu  27187  ordtoplem  28303  ordcmp  28315  heiborlem6  28741  isfldidl  28894  pridlc2  28898  mpt2bi123f  29001  mptbi12f  29005  ac6s6  29010  ctbnfien  29183  pw2f1ocnv  29412  unxpwdom3  29474  dgrsub2  29517  fmul01lt1lem1  29791  stoweidlem35  29856  stirlinglem5  29899  stirlinglem12  29906  lsatcmp  32744  lsatcmp2  32745  2atm  33267  trlatn0  33912  trlval3  33927  cdleme18c  34033  cdlemg17b  34402  cdlemg17i  34409  cdlemh  34557  dia2dimlem2  34806  dia2dimlem3  34807  dochlkr  35126  dochkrshp  35127  lcfl6  35241  lcfrlem9  35291  hdmap14lem6  35617  hgmapval0  35636