Theorem ord 367

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

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

This theorem is referenced by:  orcanai  880  oplem1  931  ecase23d  1287  19.33b  1615  eqsn  3920  disji2  4159  disjxiun  4169  pwssun  4449  swopo  4473  somo  4497  ordtri3or  4573  ordtri1  4574  ordtri3  4577  ord0eln0  4595  suc11  4644  elpwunsn  4716  ordeleqon  4728  ssonprc  4731  onmindif2  4751  limsssuc  4789  limom  4819  frsn  4907  foconst  5623  onfununi  6562  oeeulem  6803  uniinqs  6943  pw2f1olem  7171  pssnn  7286  ordtypelem9  7451  ordtypelem10  7452  oismo  7465  preleq  7528  suc11reg  7530  cantnfp1lem2  7591  cantnflem1  7601  cnfcom2lem  7614  cnfcom3lem  7616  rankxpsuc  7762  cardlim  7815  alephdom  7918  cardaleph  7926  iscard3  7930  pwcdadom  8052  cfslbn  8103  fin1a2lem12  8247  gchi  8455  fpwwe2lem13  8473  tskssel  8588  inttsk  8605  inar1  8606  r1tskina  8613  tskuni  8614  gruina  8649  grur1  8651  nlt1pi  8739  nqereu  8762  leltne  9120  nneo  10309  zeo2  10312  xrleltne  10694  nltpnft  10710  ngtmnft  10711  xrrebnd  10712  xaddf  10766  xrsupsslem  10841  xrinfmsslem  10842  seqf1olem1  11317  seqf1olem2  11318  discr1  11470  hashnncl  11600  seqcoll2  11668  sqeqd  11926  sqrmo  12012  isercoll  12416  dvdseq  12852  bitsfzo  12902  bitsinv1lem  12908  bitsf1  12913  bezoutlem3  12995  eucalglt  13031  phibndlem  13114  dfphi2  13118  prmdiv  13129  odzdvds  13136  pceq0  13199  pc2dvds  13207  fldivp1  13221  pcfac  13223  prmreclem3  13241  1arith  13250  4sqlem10  13270  4sqlem17  13284  4sqlem18  13285  vdwlem6  13309  ramubcl  13341  ramcl  13352  mrissmrcd  13820  oddvdsnn0  15137  odnncl  15138  oddvds  15140  odcl2  15156  gexdvds  15173  gexnnod  15177  sylow1lem1  15187  odcau  15193  pgpssslw  15203  efgs1b  15323  efgredlema  15327  torsubg  15424  prmcyg  15458  gsumval3eu  15468  ablfacrplem  15578  ablfac1eu  15586  lspdisj  16152  lspsncv0  16173  fidomndrnglem  16321  gzrngunitlem  16718  prmirredlem  16728  fctop  17023  cctop  17025  ppttop  17026  pptbas  17027  ordtrest2lem  17221  conclo  17431  txindis  17619  filcon  17868  ufilb  17891  cldsubg  18093  reconnlem1  18810  reconnlem2  18811  metds0  18833  metdseq0  18837  metnrmlem1a  18841  iccpnfhmeo  18923  xrhmeo  18924  cphsubrglem  19093  minveclem3b  19282  minveclem4a  19284  vitalilem4  19456  itg2gt0  19605  itgsplitioo  19682  limccnp2  19732  rollelem  19826  dvlip  19830  itgsubstlem  19885  plyaddlem1  20085  plymullem1  20086  coefv0  20119  dgreq0  20136  radcnv0  20285  pserdvlem2  20297  pilem2  20321  sineq0  20382  logtayl  20504  cxpsqr  20547  isosctrlem2  20616  atantayl2  20731  leibpilem1  20733  rlimcnp2  20758  amgm  20782  basellem3  20818  muval2  20870  sqf11  20875  ppinprm  20888  chtnprm  20890  perfectlem2  20967  lgsdir  21067  lgsabs1  21071  lgseisenlem1  21086  2sqlem7  21107  2sqblem  21114  chebbnd1lem1  21116  dchrisum0flblem1  21155  pntpbnd1  21233  pntpbnd2  21234  ostth  21286  minvecolem5  22336  staddi  23702  stadd3i  23704  atsseq  23803  atom1d  23809  atoml2i  23839  disji2f  23972  disjif2  23976  subfacp1lem6  24824  cvmscld  24913  cvmsss2  24914  cvmseu  24916  ordtoplem  26089  ordcmp  26101  heiborlem6  26415  isfldidl  26568  pridlc2  26572  ctbnfien  26769  pw2f1ocnv  26998  unxpwdom3  27124  dgrsub2  27207  psgnunilem5  27285  fmul01lt1lem1  27581  stoweidlem35  27651  stirlinglem5  27694  stirlinglem12  27701  lsatcmp  29486  lsatcmp2  29487  2atm  30009  trlatn0  30654  trlval3  30669  cdleme18c  30775  cdlemg17b  31144  cdlemg17i  31151  cdlemh  31299  dia2dimlem2  31548  dia2dimlem3  31549  dochlkr  31868  dochkrshp  31869  lcfl6  31983  lcfrlem9  32033  hdmap14lem6  32359  hgmapval0  32378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-or 360