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  simprld  530  simprrd  532  simp2  1000  simp3  1001  sbh  1798  eldifbd  3177  unssbd  3350  opth  4280  potr  4354  frind  4398  brrelex2  4715  funinsn  5322  feu  5457  fcnvres  5458  fun11iun  5542  funopsn  5761  elmpocl2  6142  uchoice  6222  oprssdmm  6256  tfrlem1  6393  tfrlemisucfn  6409  tfrlemisucaccv  6410  tfrlemibxssdm  6412  tfrlemibfn  6413  tfrlemi14d  6418  swoer  6647  elmapssres  6759  mapsspm  6768  pmsspw  6769  mapss  6777  dom0  6934  xpf1o  6940  sbthlemi8  7065  sbthlemi9  7066  supelti  7103  supisoti  7111  djulclb  7156  nninfninc  7224  nnnninfeq2  7230  cardcl  7287  isnumi  7288  cardval3ex  7291  exmidonfinlem  7300  en2eleq  7302  finacn  7315  acfun  7318  exmidaclem  7319  dftap2  7362  exmidapne  7371  ccfunen  7375  acnccim  7383  indpi  7454  dfplpq2  7466  ltbtwnnq  7528  enq0tr  7546  nqnq0pi  7550  elnp1st2nd  7588  prcunqu  7597  prnmaxl  7600  prloc  7603  genpcuu  7632  addnqprllem  7639  addlocprlemeq  7645  addlocprlemgt  7646  addlocpr  7648  nqprxx  7658  gtnqex  7662  appdivnq  7675  prmuloclemcalc  7677  prmuloc  7678  mullocprlem  7682  ltprordil  7701  ltnqpri  7706  ltexprlemm  7712  ltexprlemopl  7713  ltexprlemlol  7714  ltexprlemopu  7715  ltexprlemupu  7716  ltexprlemdisj  7718  ltexprlemloc  7719  ltexprlemfl  7721  ltexprlemrl  7722  ltexprlemfu  7723  ltexprlemru  7724  ltexpri  7725  recexprlemell  7734  recexprlemelu  7735  recexprlemloc  7743  recexprlempr  7744  recexprlem1ssl  7745  recexprlem1ssu  7746  recexprlemss1l  7747  aptipr  7753  cauappcvgprlemlol  7759  cauappcvgprlemupu  7761  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  cauappcvgprlemladdrl  7769  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemlol  7782  caucvgprlemupu  7784  caucvgprlemladdfu  7789  caucvgprlem1  7791  caucvgprlem2  7792  caucvgprprlemnjltk  7803  caucvgprprlemnbj  7805  caucvgprprlemlol  7810  caucvgprprlemupu  7812  caucvgprprlemexbt  7818  caucvgprprlem1  7821  caucvgprprlem2  7822  suplocexprlemrl  7829  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemub  7835  suplocexprlemlub  7836  ltsrprg  7859  gt0srpr  7860  recexgt0sr  7885  addgt0sr  7887  mulgt0sr  7890  map2psrprg  7917  suplocsrlemb  7918  suplocsrlem  7920  nnindnn  8005  axcaucvglemcau  8010  axpre-suploclemres  8013  apreap  8659  apreim  8675  mulge0  8691  apti  8694  mulap0bbd  8732  lble  9019  nnind  9051  recnz  9465  uzind  9483  eluzadd  9676  eluzsub  9677  ixxss1  10025  ixxss2  10026  ixxss12  10027  iccss2  10065  iccssioo2  10067  iccssico2  10068  elfzolt2  10278  infssuzcldc  10376  ioom  10401  elicore  10407  flqltp1  10420  addmodlteq  10541  expcl2lemap  10694  expap0i  10714  hashennnuni  10922  hashdmprop2dom  10987  wrdexb  11004  crre  11139  caucvgre  11263  cvg1nlemcau  11266  cvg1nlemres  11267  resqrexlemoverl  11303  sqrtge0  11315  fimaxre2  11509  climi  11569  reccn2ap  11595  climge0  11607  nnf1o  11658  sumpr  11695  fsump1i  11715  fsum00  11744  fsumparts  11752  mertenslemi1  11817  addsin  12024  subsin  12025  addcos  12028  subcos  12029  sinbnd2  12036  cosbnd2  12037  sinltxirr  12043  dvdsaddre2b  12123  evenelz  12149  4dvdseven  12199  gcd0id  12271  gcd1  12279  bezoutlemstep  12289  dvdsgcdb  12305  mulgcd  12308  gcdzeq  12314  dvdsmulgcd  12317  sqgcd  12321  dvdssqlem  12322  bezoutr  12324  uzwodc  12329  nninfctlemfo  12332  lcmval  12356  lcmcllem  12360  lcmgcdlem  12370  lcmdvds  12372  lcmgcdeq  12376  lcmdvdsb  12377  mulgcddvds  12387  rpmulgcd2  12388  qredeu  12390  rpdvds  12392  divgcdcoprm0  12394  isprm3  12411  divgcdodd  12436  coprm  12437  rpexp  12446  sqrt2irr  12455  qdencl  12482  qeqnumdivden  12487  divnumden  12489  divdenle  12490  densq  12497  phimullem  12518  eulerthlem1  12520  eulerthlemrprm  12522  eulerthlemth  12525  prmdiveq  12529  prmdivdiv  12530  hashgcdeq  12533  phisum  12534  odzid  12538  reumodprminv  12547  oddn2prm  12555  pythagtriplem4  12562  pythagtriplem11  12568  pythagtriplem13  12570  pythagtriplem19  12576  pclemub  12581  pcprendvds2  12585  pcpre1  12586  pcpremul  12587  pceulem  12588  pczdvds  12608  pc2dvds  12624  pcaddlem  12633  pcmpt  12637  pcmpt2  12638  pcmptdvds  12639  pcprod  12640  pockthlem  12650  pockthg  12651  prmunb  12656  1arithlem4  12660  4sqlem7  12678  4sqlem8  12679  4sqlem9  12680  4sqlem10  12681  4sqlemffi  12690  4sqlem15  12699  4sqlem16  12700  4sqlem17  12701  4sqlem18  12702  ennnfonelemom  12750  ennnfonelemex  12756  ennnfonelemf1  12760  ctiunctlemu1st  12776  ctiunctlemu2nd  12777  fnpr2ob  13143  mgmlrid  13182  gsumfzval  13194  gsumval2  13200  mndrid  13239  prdsmndd  13251  grpinvcnv  13371  dfgrp3mlem  13401  prdsgrpd  13412  prdsinvgd  13413  eqglact  13532  ghmgrp2  13553  ghmlin  13555  ghmnsgpreima  13576  kerf1ghm  13581  srgdilem  13702  srgdir  13708  srgridm  13713  ringdilem  13745  ringdir  13752  ringridm  13757  unitmulcl  13846  unitnegcl  13863  rhmmhm  13892  elrhmunit  13910  lringuplu  13929  subrgring  13957  subrg1cl  13962  qusrhm  14261  znunit  14392  znrrg  14393  psrelbas  14408  mplsubgfilemcl  14432  mplsubgfileminv  14433  inopn  14446  restbasg  14611  ssrest  14625  cntop2  14645  icnpimaex  14654  cnima  14663  lmfss  14687  lmtopcnp  14693  txhmeo  14762  txswaphmeo  14764  psmet0  14770  psmettri2  14771  blhalf  14851  bdxmet  14944  xmetxpbl  14951  ioo2bl  14994  tgioo  14997  cncfi  15021  rescncf  15024  cdivcncfap  15047  cnopnap  15054  divcncfap  15057  dedekindeulemeu  15065  dedekindicclemeu  15074  ivthinclemum  15078  ivthinclemlopn  15079  ivthinclemuopn  15081  ivthinclemdisj  15083  ivthdec  15087  ivthreinc  15088  limcimo  15108  cnplimcim  15110  cnplimclemr  15112  cnlimci  15116  limccnpcntop  15118  limccnp2lem  15119  limccnp2cntop  15120  limccoap  15121  reldvg  15122  dvbsssg  15129  dvfgg  15131  dvaddxxbr  15144  dvmulxxbr  15145  dvcoapbr  15150  dvcjbr  15151  dvrecap  15156  plyco  15202  plycj  15204  plyrecj  15206  sin0pilem1  15224  sin0pilem2  15225  tanrpcl  15280  tangtx  15281  cos0pilt1  15295  logbgcd1irraplemexp  15411  mpodvdsmulf1o  15433  perfect  15444  lgsne0  15486  lgseisen  15522  lgsquad2lem2  15530  2sqlem8a  15570  2sqlem8  15571  structgrssiedg  15611  bj-charfunbi  15709  bj-inf2vnlem1  15868  pwf1oexmid  15898  subctctexmid  15899  iooref1o  15935  taupi  15974  alsi2d  15983  alsc2d  15985