Theorem ord 392

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

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

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 197  df-or 385

This theorem is referenced by:  ornld  940  orcanai  952  oplem1  1007  ecase23d  1436  19.33b  1813  elpwunsn  4224  eqsnOLD  4362  disji2  4636  disjxiun  4649  disjxiunOLD  4650  pwssun  5020  swopo  5045  sotric  5061  sotrieq  5062  somo  5069  ordtri3or  5755  ordtri1  5756  ordtri3OLD  5760  suc11  5831  foconst  6126  ordeleqon  6988  ssonprc  6992  onmindif2  7012  limsssuc  7050  limom  7080  onfununi  7438  oeeulem  7681  uniinqs  7827  pw2f1olem  8064  pssnn  8178  ordtypelem9  8431  ordtypelem10  8432  oismo  8445  preleq  8514  suc11reg  8516  cantnfp1lem2  8576  cantnflem1  8586  cnfcom2lem  8598  cnfcom3lem  8600  rankxpsuc  8745  cardlim  8798  alephdom  8904  cardaleph  8912  iscard3  8916  pwcdadom  9038  cfslbn  9089  fin1a2lem12  9233  gchi  9446  fpwwe2lem13  9464  tskssel  9579  inttsk  9596  inar1  9597  r1tskina  9604  tskuni  9605  gruina  9640  grur1  9642  nlt1pi  9728  nqereu  9751  leltne  10127  nneo  11461  zeo2  11464  xrleltne  11978  nltpnft  11995  ngtmnft  11997  xrrebnd  11999  xaddf  12055  xrsupsslem  12137  xrinfmsslem  12138  fzocatel  12531  seqf1olem1  12840  seqf1olem2  12841  discr1  13000  hashnncl  13157  seqcoll2  13249  sqeqd  13906  sqrmo  13992  isercoll  14398  bitsfzo  15157  bitsinv1lem  15163  bitsf1  15168  bezoutlem3  15258  eucalglt  15298  phibndlem  15475  dfphi2  15479  prmdiv  15490  odzdvds  15500  pceq0  15575  pc2dvds  15583  fldivp1  15601  pcfac  15603  prmreclem3  15622  1arith  15631  4sqlem10  15651  4sqlem17  15665  4sqlem18  15666  vdwlem6  15690  ramubcl  15722  ramcl  15733  mrissmrcd  16300  psgnunilem5  17914  oddvdsnn0  17963  odnncl  17964  oddvds  17966  odcl2  17982  gexdvds  17999  gexnnod  18003  sylow1lem1  18013  odcau  18019  pgpssslw  18029  efgs1b  18149  efgredlema  18153  torsubg  18257  prmcyg  18295  gsumval3eu  18305  ablfacrplem  18464  ablfac1eu  18472  lspdisj  19125  lspsncv0  19146  fidomndrnglem  19306  gzrngunitlem  19811  prmirredlem  19841  fctop  20808  cctop  20810  ppttop  20811  pptbas  20812  ordtrest2lem  21007  connclo  21218  txindis  21437  filconn  21687  ufilb  21710  cldsubg  21914  reconnlem1  22629  reconnlem2  22630  metds0  22653  metdseq0  22657  metnrmlem1a  22661  iccpnfhmeo  22744  xrhmeo  22745  cphsubrglem  22977  minveclem3b  23199  minveclem4a  23201  vitalilem4  23380  itg2gt0  23527  itgsplitioo  23604  limccnp2  23656  rollelem  23752  dvlip  23756  itgsubstlem  23811  plyaddlem1  23969  plymullem1  23970  coefv0  24004  dgreq0  24021  radcnv0  24170  pserdvlem2  24182  pilem2  24206  sineq0  24273  logtayl  24406  cxpsqrt  24449  isosctrlem2  24549  atantayl2  24665  leibpilem1  24667  rlimcnp2  24693  amgm  24717  basellem3  24809  muval2  24860  sqf11  24865  ppinprm  24878  chtnprm  24880  perfectlem2  24955  lgsdir  25057  lgsabs1  25061  lgseisenlem1  25100  2sqlem7  25149  2sqblem  25156  chebbnd1lem1  25158  dchrisum0flblem1  25197  pntpbnd1  25275  pntpbnd2  25276  ostth  25328  symquadlem  25584  midexlem  25587  colperp  25621  midex  25629  oppperpex  25645  outpasch  25647  hlpasch  25648  hpgerlem  25657  colopp  25661  colhp  25662  lmieu  25676  lmicom  25680  trgcopy  25696  cgracol  25719  minvecolem5  27737  staddi  29105  stadd3i  29107  atsseq  29206  atom1d  29212  atoml2i  29242  disji2f  29390  disjif2  29394  znsqcld  29512  fprodex01  29571  2sqmod  29648  psgnfzto1stlem  29850  ordtrest2NEWlem  29968  eulerpartlemb  30430  sgn3da  30603  subfacp1lem6  31167  cvmscld  31255  cvmsss2  31256  cvmseu  31258  nosepon  31818  ordtoplem  32434  ordcmp  32446  poimirlem25  33434  heiborlem6  33615  isfldidl  33867  pridlc2  33871  mpt2bi123f  33971  mptbi12f  33975  ac6s6  33980  lsatcmp  34290  lsatcmp2  34291  2atm  34813  trlatn0  35459  trlval3  35474  cdleme18c  35580  cdlemg17b  35950  cdlemg17i  35957  cdlemh  36105  dia2dimlem2  36354  dia2dimlem3  36355  dochlkr  36674  dochkrshp  36675  lcfl6  36789  lcfrlem9  36839  hdmap14lem6  37165  hgmapval0  37184  ctbnfien  37382  pw2f1ocnv  37604  unxpwdom3  37665  dgrsub2  37705  rp-fakeanorass  37858  disjxp1  39238  fmul01lt1lem1  39816  elprn1  39865  stoweidlem35  40252  stirlinglem5  40295  stirlinglem12  40302  fourierdlem42  40366  fourierdlem93  40416  perfectALTVlem2  41631