Theorem simprd 114

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
simprd.1	|- ( ph -> ( ps /\ ch ) )

Assertion

Ref	Expression
simprd	|- ( ph -> ch )

Proof of Theorem simprd

Step	Hyp	Ref	Expression
1		simprd.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		simpr 110	. 2 |- ( ( ps /\ ch ) -> ch )
3	1, 2	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107

This theorem is referenced by:  biimpr  130  simprbi  275  simplbda  384  simplrd  530  simprld  532  simprrd  534  simp2  1025  simp3  1026  sbh  1824  eldifbd  3213  unssbd  3387  opth  4335  potr  4411  frind  4455  brrelex2  4773  funinsn  5386  feu  5527  fcnvres  5528  fun11iun  5613  funopsn  5838  elmpocl2  6229  uchoice  6309  oprssdmm  6343  fczsupp0  6437  tfrlem1  6517  tfrlemisucfn  6533  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemi14d  6542  swoer  6773  elmapssres  6885  mapsspm  6894  pmsspw  6895  mapss  6903  dom0  7067  xpf1o  7073  sbthlemi8  7206  sbthlemi9  7207  supelti  7244  supisoti  7252  djulclb  7297  nninfninc  7365  nnnninfeq2  7371  cardcl  7428  isnumi  7429  cardval3ex  7432  exmidonfinlem  7447  en2eleq  7449  finacn  7462  acfun  7465  exmidaclem  7466  pw1if  7486  dftap2  7513  exmidapne  7522  ccfunen  7526  acnccim  7534  indpi  7605  dfplpq2  7617  ltbtwnnq  7679  enq0tr  7697  nqnq0pi  7701  elnp1st2nd  7739  prcunqu  7748  prnmaxl  7751  prloc  7754  genpcuu  7783  addnqprllem  7790  addlocprlemeq  7796  addlocprlemgt  7797  addlocpr  7799  nqprxx  7809  gtnqex  7813  appdivnq  7826  prmuloclemcalc  7828  prmuloc  7829  mullocprlem  7833  ltprordil  7852  ltnqpri  7857  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  ltexpri  7876  recexprlemell  7885  recexprlemelu  7886  recexprlemloc  7894  recexprlempr  7895  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1l  7898  aptipr  7904  cauappcvgprlemlol  7910  cauappcvgprlemupu  7912  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdrl  7920  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemlol  7933  caucvgprlemupu  7935  caucvgprlemladdfu  7940  caucvgprlem1  7942  caucvgprlem2  7943  caucvgprprlemnjltk  7954  caucvgprprlemnbj  7956  caucvgprprlemlol  7961  caucvgprprlemupu  7963  caucvgprprlemexbt  7969  caucvgprprlem1  7972  caucvgprprlem2  7973  suplocexprlemrl  7980  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemub  7986  suplocexprlemlub  7987  ltsrprg  8010  gt0srpr  8011  recexgt0sr  8036  addgt0sr  8038  mulgt0sr  8041  map2psrprg  8068  suplocsrlemb  8069  suplocsrlem  8071  nnindnn  8156  axcaucvglemcau  8161  axpre-suploclemres  8164  apreap  8809  apreim  8825  mulge0  8841  apti  8844  mulap0bbd  8882  lble  9169  nnind  9201  recnz  9617  uzind  9635  eluzadd  9829  eluzsub  9830  ixxss1  10183  ixxss2  10184  ixxss12  10185  iccss2  10223  iccssioo2  10225  iccssico2  10226  elfzolt2  10437  infssuzcldc  10541  ioom  10566  elicore  10572  flqltp1  10585  addmodlteq  10706  expcl2lemap  10859  expap0i  10879  hashennnuni  11087  hashdmprop2dom  11154  wrdexb  11174  swrdsbslen  11296  swrdspsleq  11297  crre  11480  caucvgre  11604  cvg1nlemcau  11607  cvg1nlemres  11608  resqrexlemoverl  11644  sqrtge0  11656  fimaxre2  11850  climi  11910  reccn2ap  11936  climge0  11948  nnf1o  12000  sumpr  12037  fsump1i  12057  fsum00  12086  fsumparts  12094  mertenslemi1  12159  addsin  12366  subsin  12367  addcos  12370  subcos  12371  sinbnd2  12378  cosbnd2  12379  sinltxirr  12385  dvdsaddre2b  12465  evenelz  12491  4dvdseven  12541  gcd0id  12613  gcd1  12621  bezoutlemstep  12631  dvdsgcdb  12647  mulgcd  12650  gcdzeq  12656  dvdsmulgcd  12659  sqgcd  12663  dvdssqlem  12664  bezoutr  12666  uzwodc  12671  nninfctlemfo  12674  lcmval  12698  lcmcllem  12702  lcmgcdlem  12712  lcmdvds  12714  lcmgcdeq  12718  lcmdvdsb  12719  mulgcddvds  12729  rpmulgcd2  12730  qredeu  12732  rpdvds  12734  divgcdcoprm0  12736  isprm3  12753  divgcdodd  12778  coprm  12779  rpexp  12788  sqrt2irr  12797  qdencl  12824  qeqnumdivden  12829  divnumden  12831  divdenle  12832  densq  12839  phimullem  12860  eulerthlem1  12862  eulerthlemrprm  12864  eulerthlemth  12867  prmdiveq  12871  prmdivdiv  12872  hashgcdeq  12875  phisum  12876  odzid  12880  reumodprminv  12889  oddn2prm  12897  pythagtriplem4  12904  pythagtriplem11  12910  pythagtriplem13  12912  pythagtriplem19  12918  pclemub  12923  pcprendvds2  12927  pcpre1  12928  pcpremul  12929  pceulem  12930  pczdvds  12950  pc2dvds  12966  pcaddlem  12975  pcmpt  12979  pcmpt2  12980  pcmptdvds  12981  pcprod  12982  pockthlem  12992  pockthg  12993  prmunb  12998  1arithlem4  13002  4sqlem7  13020  4sqlem8  13021  4sqlem9  13022  4sqlem10  13023  4sqlemffi  13032  4sqlem15  13041  4sqlem16  13042  4sqlem17  13043  4sqlem18  13044  ennnfonelemom  13092  ennnfonelemex  13098  ennnfonelemf1  13102  ctiunctlemu1st  13118  ctiunctlemu2nd  13119  fnpr2ob  13486  mgmlrid  13525  gsumfzval  13537  gsumval2  13543  mndrid  13582  prdsmndd  13594  grpinvcnv  13714  dfgrp3mlem  13744  prdsgrpd  13755  prdsinvgd  13756  eqglact  13875  ghmgrp2  13896  ghmlin  13898  ghmnsgpreima  13919  kerf1ghm  13924  gsumsplit0  13996  srgdilem  14046  srgdir  14052  srgridm  14057  ringdilem  14089  ringdir  14096  ringridm  14101  unitmulcl  14191  unitnegcl  14208  rhmmhm  14237  elrhmunit  14255  lringuplu  14274  subrgring  14302  subrg1cl  14307  qusrhm  14607  znunit  14738  znrrg  14739  psrbaglecl  14754  psrbagcon  14755  psrbagconcl  14756  psrelbas  14759  mplsubgfilemcl  14783  mplsubgfileminv  14784  inopn  14797  restbasg  14962  ssrest  14976  cntop2  14996  icnpimaex  15005  cnima  15014  lmfss  15038  lmtopcnp  15044  txhmeo  15113  txswaphmeo  15115  psmet0  15121  psmettri2  15122  blhalf  15202  bdxmet  15295  xmetxpbl  15302  ioo2bl  15345  tgioo  15348  cncfi  15372  rescncf  15375  cdivcncfap  15398  cnopnap  15405  divcncfap  15408  dedekindeulemeu  15416  dedekindicclemeu  15425  ivthinclemum  15429  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthinclemdisj  15434  ivthdec  15438  ivthreinc  15439  limcimo  15459  cnplimcim  15461  cnplimclemr  15463  cnlimci  15467  limccnpcntop  15469  limccnp2lem  15470  limccnp2cntop  15471  limccoap  15472  reldvg  15473  dvbsssg  15480  dvfgg  15482  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  dvrecap  15507  plyco  15553  plycj  15555  plyrecj  15557  sin0pilem1  15575  sin0pilem2  15576  tanrpcl  15631  tangtx  15632  cos0pilt1  15646  logbgcd1irraplemexp  15762  mpodvdsmulf1o  15787  perfect  15798  lgsne0  15840  lgseisen  15876  lgsquad2lem2  15884  2sqlem8a  15924  2sqlem8  15925  structgrssiedg  15967  uhgrm  16002  umgredgne  16074  usgruspgrben  16110  usgredgppren  16121  umgr2edg  16131  vtxdumgrfival  16222  wlkpropg  16248  wlkv  16250  wlkvtxeledgg  16268  g0wlk0  16294  trlsv  16308  clwwlknlen  16335  eupthv  16370  eupthf1o  16374  eupth2lem3lem4fi  16397  eulerpathprum  16404  bj-charfunbi  16510  bj-inf2vnlem1  16669  pwf1oexmid  16704  subctctexmid  16705  iooref1o  16749  taupi  16789  alsi2d  16808  alsc2d  16810