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  998  simp3  999  sbh  1776  eldifbd  3141  unssbd  3313  opth  4237  potr  4308  frind  4352  brrelex2  4667  funinsn  5265  feu  5398  fcnvres  5399  fun11iun  5482  elmpocl2  6070  oprssdmm  6171  tfrlem1  6308  tfrlemisucfn  6324  tfrlemisucaccv  6325  tfrlemibxssdm  6327  tfrlemibfn  6328  tfrlemi14d  6333  swoer  6562  elmapssres  6672  mapsspm  6681  pmsspw  6682  mapss  6690  dom0  6837  xpf1o  6843  sbthlemi8  6962  sbthlemi9  6963  supelti  7000  supisoti  7008  djulclb  7053  nnnninfeq2  7126  cardcl  7179  isnumi  7180  cardval3ex  7183  exmidonfinlem  7191  en2eleq  7193  acfun  7205  exmidaclem  7206  dftap2  7249  exmidapne  7258  ccfunen  7262  indpi  7340  dfplpq2  7352  ltbtwnnq  7414  enq0tr  7432  nqnq0pi  7436  elnp1st2nd  7474  prcunqu  7483  prnmaxl  7486  prloc  7489  genpcuu  7518  addnqprllem  7525  addlocprlemeq  7531  addlocprlemgt  7532  addlocpr  7534  nqprxx  7544  gtnqex  7548  appdivnq  7561  prmuloclemcalc  7563  prmuloc  7564  mullocprlem  7568  ltprordil  7587  ltnqpri  7592  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemlol  7600  ltexprlemopu  7601  ltexprlemupu  7602  ltexprlemdisj  7604  ltexprlemloc  7605  ltexprlemfl  7607  ltexprlemrl  7608  ltexprlemfu  7609  ltexprlemru  7610  ltexpri  7611  recexprlemell  7620  recexprlemelu  7621  recexprlemloc  7629  recexprlempr  7630  recexprlem1ssl  7631  recexprlem1ssu  7632  recexprlemss1l  7633  aptipr  7639  cauappcvgprlemlol  7645  cauappcvgprlemupu  7647  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdrl  7655  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemlol  7668  caucvgprlemupu  7670  caucvgprlemladdfu  7675  caucvgprlem1  7677  caucvgprlem2  7678  caucvgprprlemnjltk  7689  caucvgprprlemnbj  7691  caucvgprprlemlol  7696  caucvgprprlemupu  7698  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  suplocexprlemrl  7715  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemub  7721  suplocexprlemlub  7722  ltsrprg  7745  gt0srpr  7746  recexgt0sr  7771  addgt0sr  7773  mulgt0sr  7776  map2psrprg  7803  suplocsrlemb  7804  suplocsrlem  7806  nnindnn  7891  axcaucvglemcau  7896  axpre-suploclemres  7899  apreap  8543  apreim  8559  mulge0  8575  apti  8578  mulap0bbd  8616  lble  8903  nnind  8934  recnz  9345  uzind  9363  eluzadd  9555  eluzsub  9556  ixxss1  9903  ixxss2  9904  ixxss12  9905  iccss2  9943  iccssioo2  9945  iccssico2  9946  elfzolt2  10155  ioom  10260  elicore  10266  flqltp1  10278  addmodlteq  10397  expcl2lemap  10531  expap0i  10551  hashennnuni  10758  crre  10865  caucvgre  10989  cvg1nlemcau  10992  cvg1nlemres  10993  resqrexlemoverl  11029  sqrtge0  11041  fimaxre2  11234  climi  11294  reccn2ap  11320  climge0  11332  nnf1o  11383  sumpr  11420  fsump1i  11440  fsum00  11469  fsumparts  11477  mertenslemi1  11542  addsin  11749  subsin  11750  addcos  11753  subcos  11754  sinbnd2  11761  cosbnd2  11762  dvdsaddre2b  11847  evenelz  11871  4dvdseven  11921  infssuzcldc  11951  gcd0id  11979  gcd1  11987  bezoutlemstep  11997  dvdsgcdb  12013  mulgcd  12016  gcdzeq  12022  dvdsmulgcd  12025  sqgcd  12029  dvdssqlem  12030  bezoutr  12032  uzwodc  12037  lcmval  12062  lcmcllem  12066  lcmgcdlem  12076  lcmdvds  12078  lcmgcdeq  12082  lcmdvdsb  12083  mulgcddvds  12093  rpmulgcd2  12094  qredeu  12096  rpdvds  12098  divgcdcoprm0  12100  isprm3  12117  divgcdodd  12142  coprm  12143  rpexp  12152  sqrt2irr  12161  qdencl  12188  qeqnumdivden  12193  divnumden  12195  divdenle  12196  densq  12203  phimullem  12224  eulerthlem1  12226  eulerthlemrprm  12228  eulerthlemth  12231  prmdiveq  12235  prmdivdiv  12236  hashgcdeq  12238  phisum  12239  odzid  12243  reumodprminv  12252  oddn2prm  12260  pythagtriplem4  12267  pythagtriplem11  12273  pythagtriplem13  12275  pythagtriplem19  12281  pclemub  12286  pcprendvds2  12290  pcpre1  12291  pcpremul  12292  pceulem  12293  pczdvds  12312  pc2dvds  12328  pcaddlem  12337  pcmpt  12340  pcmpt2  12341  pcmptdvds  12342  pcprod  12343  pockthlem  12353  pockthg  12354  prmunb  12359  1arithlem4  12363  4sqlem7  12381  4sqlem8  12382  4sqlem9  12383  4sqlem10  12384  ennnfonelemom  12408  ennnfonelemex  12414  ennnfonelemf1  12418  ctiunctlemu1st  12434  ctiunctlemu2nd  12435  fnpr2ob  12758  mgmlrid  12797  mndrid  12836  grpinvcnv  12937  dfgrp3mlem  12967  eqglact  13082  srgdilem  13150  srgdir  13156  srgridm  13161  ringdilem  13193  ringdir  13200  ringridm  13205  unitmulcl  13280  unitnegcl  13297  lringuplu  13335  subrgring  13343  subrg1cl  13348  inopn  13473  restbasg  13638  ssrest  13652  cntop2  13672  icnpimaex  13681  cnima  13690  lmfss  13714  lmtopcnp  13720  txhmeo  13789  txswaphmeo  13791  psmet0  13797  psmettri2  13798  blhalf  13878  bdxmet  13971  xmetxpbl  13978  ioo2bl  14013  tgioo  14016  cncfi  14035  rescncf  14038  cdivcncfap  14057  cnopnap  14064  dedekindeulemeu  14070  dedekindicclemeu  14079  ivthinclemum  14083  ivthinclemlopn  14084  ivthinclemuopn  14086  ivthinclemdisj  14088  ivthdec  14092  limcimo  14104  cnplimcim  14106  cnplimclemr  14108  cnlimci  14112  limccnpcntop  14114  limccnp2lem  14115  limccnp2cntop  14116  limccoap  14117  reldvg  14118  dvbsssg  14125  dvfgg  14127  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvcjbr  14142  dvrecap  14147  sin0pilem1  14172  sin0pilem2  14173  tanrpcl  14228  tangtx  14229  cos0pilt1  14243  logbgcd1irraplemexp  14356  lgsne0  14409  2sqlem8a  14439  2sqlem8  14440  bj-charfunbi  14533  bj-inf2vnlem1  14692  pwf1oexmid  14719  subctctexmid  14720  iooref1o  14752  taupi  14790  alsi2d  14799  alsc2d  14801