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  1022  simp3  1023  sbh  1822  eldifbd  3210  unssbd  3383  opth  4327  potr  4403  frind  4447  brrelex2  4765  funinsn  5376  feu  5516  fcnvres  5517  fun11iun  5601  funopsn  5825  elmpocl2  6214  uchoice  6295  oprssdmm  6329  tfrlem1  6469  tfrlemisucfn  6485  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrlemi14d  6494  swoer  6725  elmapssres  6837  mapsspm  6846  pmsspw  6847  mapss  6855  dom0  7019  xpf1o  7025  sbthlemi8  7154  sbthlemi9  7155  supelti  7192  supisoti  7200  djulclb  7245  nninfninc  7313  nnnninfeq2  7319  cardcl  7376  isnumi  7377  cardval3ex  7380  exmidonfinlem  7394  en2eleq  7396  finacn  7409  acfun  7412  exmidaclem  7413  pw1if  7433  dftap2  7460  exmidapne  7469  ccfunen  7473  acnccim  7481  indpi  7552  dfplpq2  7564  ltbtwnnq  7626  enq0tr  7644  nqnq0pi  7648  elnp1st2nd  7686  prcunqu  7695  prnmaxl  7698  prloc  7701  genpcuu  7730  addnqprllem  7737  addlocprlemeq  7743  addlocprlemgt  7744  addlocpr  7746  nqprxx  7756  gtnqex  7760  appdivnq  7773  prmuloclemcalc  7775  prmuloc  7776  mullocprlem  7780  ltprordil  7799  ltnqpri  7804  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  ltexpri  7823  recexprlemell  7832  recexprlemelu  7833  recexprlemloc  7841  recexprlempr  7842  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1l  7845  aptipr  7851  cauappcvgprlemlol  7857  cauappcvgprlemupu  7859  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdrl  7867  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemlol  7880  caucvgprlemupu  7882  caucvgprlemladdfu  7887  caucvgprlem1  7889  caucvgprlem2  7890  caucvgprprlemnjltk  7901  caucvgprprlemnbj  7903  caucvgprprlemlol  7908  caucvgprprlemupu  7910  caucvgprprlemexbt  7916  caucvgprprlem1  7919  caucvgprprlem2  7920  suplocexprlemrl  7927  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemub  7933  suplocexprlemlub  7934  ltsrprg  7957  gt0srpr  7958  recexgt0sr  7983  addgt0sr  7985  mulgt0sr  7988  map2psrprg  8015  suplocsrlemb  8016  suplocsrlem  8018  nnindnn  8103  axcaucvglemcau  8108  axpre-suploclemres  8111  apreap  8757  apreim  8773  mulge0  8789  apti  8792  mulap0bbd  8830  lble  9117  nnind  9149  recnz  9563  uzind  9581  eluzadd  9775  eluzsub  9776  ixxss1  10129  ixxss2  10130  ixxss12  10131  iccss2  10169  iccssioo2  10171  iccssico2  10172  elfzolt2  10382  infssuzcldc  10485  ioom  10510  elicore  10516  flqltp1  10529  addmodlteq  10650  expcl2lemap  10803  expap0i  10823  hashennnuni  11031  hashdmprop2dom  11098  wrdexb  11115  swrdsbslen  11237  swrdspsleq  11238  crre  11408  caucvgre  11532  cvg1nlemcau  11535  cvg1nlemres  11536  resqrexlemoverl  11572  sqrtge0  11584  fimaxre2  11778  climi  11838  reccn2ap  11864  climge0  11876  nnf1o  11927  sumpr  11964  fsump1i  11984  fsum00  12013  fsumparts  12021  mertenslemi1  12086  addsin  12293  subsin  12294  addcos  12297  subcos  12298  sinbnd2  12305  cosbnd2  12306  sinltxirr  12312  dvdsaddre2b  12392  evenelz  12418  4dvdseven  12468  gcd0id  12540  gcd1  12548  bezoutlemstep  12558  dvdsgcdb  12574  mulgcd  12577  gcdzeq  12583  dvdsmulgcd  12586  sqgcd  12590  dvdssqlem  12591  bezoutr  12593  uzwodc  12598  nninfctlemfo  12601  lcmval  12625  lcmcllem  12629  lcmgcdlem  12639  lcmdvds  12641  lcmgcdeq  12645  lcmdvdsb  12646  mulgcddvds  12656  rpmulgcd2  12657  qredeu  12659  rpdvds  12661  divgcdcoprm0  12663  isprm3  12680  divgcdodd  12705  coprm  12706  rpexp  12715  sqrt2irr  12724  qdencl  12751  qeqnumdivden  12756  divnumden  12758  divdenle  12759  densq  12766  phimullem  12787  eulerthlem1  12789  eulerthlemrprm  12791  eulerthlemth  12794  prmdiveq  12798  prmdivdiv  12799  hashgcdeq  12802  phisum  12803  odzid  12807  reumodprminv  12816  oddn2prm  12824  pythagtriplem4  12831  pythagtriplem11  12837  pythagtriplem13  12839  pythagtriplem19  12845  pclemub  12850  pcprendvds2  12854  pcpre1  12855  pcpremul  12856  pceulem  12857  pczdvds  12877  pc2dvds  12893  pcaddlem  12902  pcmpt  12906  pcmpt2  12907  pcmptdvds  12908  pcprod  12909  pockthlem  12919  pockthg  12920  prmunb  12925  1arithlem4  12929  4sqlem7  12947  4sqlem8  12948  4sqlem9  12949  4sqlem10  12950  4sqlemffi  12959  4sqlem15  12968  4sqlem16  12969  4sqlem17  12970  4sqlem18  12971  ennnfonelemom  13019  ennnfonelemex  13025  ennnfonelemf1  13029  ctiunctlemu1st  13045  ctiunctlemu2nd  13046  fnpr2ob  13413  mgmlrid  13452  gsumfzval  13464  gsumval2  13470  mndrid  13509  prdsmndd  13521  grpinvcnv  13641  dfgrp3mlem  13671  prdsgrpd  13682  prdsinvgd  13683  eqglact  13802  ghmgrp2  13823  ghmlin  13825  ghmnsgpreima  13846  kerf1ghm  13851  srgdilem  13972  srgdir  13978  srgridm  13983  ringdilem  14015  ringdir  14022  ringridm  14027  unitmulcl  14117  unitnegcl  14134  rhmmhm  14163  elrhmunit  14181  lringuplu  14200  subrgring  14228  subrg1cl  14233  qusrhm  14532  znunit  14663  znrrg  14664  psrelbas  14679  mplsubgfilemcl  14703  mplsubgfileminv  14704  inopn  14717  restbasg  14882  ssrest  14896  cntop2  14916  icnpimaex  14925  cnima  14934  lmfss  14958  lmtopcnp  14964  txhmeo  15033  txswaphmeo  15035  psmet0  15041  psmettri2  15042  blhalf  15122  bdxmet  15215  xmetxpbl  15222  ioo2bl  15265  tgioo  15268  cncfi  15292  rescncf  15295  cdivcncfap  15318  cnopnap  15325  divcncfap  15328  dedekindeulemeu  15336  dedekindicclemeu  15345  ivthinclemum  15349  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthinclemdisj  15354  ivthdec  15358  ivthreinc  15359  limcimo  15379  cnplimcim  15381  cnplimclemr  15383  cnlimci  15387  limccnpcntop  15389  limccnp2lem  15390  limccnp2cntop  15391  limccoap  15392  reldvg  15393  dvbsssg  15400  dvfgg  15402  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvrecap  15427  plyco  15473  plycj  15475  plyrecj  15477  sin0pilem1  15495  sin0pilem2  15496  tanrpcl  15551  tangtx  15552  cos0pilt1  15566  logbgcd1irraplemexp  15682  mpodvdsmulf1o  15704  perfect  15715  lgsne0  15757  lgseisen  15793  lgsquad2lem2  15801  2sqlem8a  15841  2sqlem8  15842  structgrssiedg  15884  uhgrm  15919  umgredgne  15989  usgruspgrben  16025  usgredgppren  16036  umgr2edg  16046  vtxdumgrfival  16104  wlkpropg  16121  wlkv  16123  wlkvtxeledgg  16141  g0wlk0  16167  trlsv  16179  clwwlknlen  16206  eupthv  16241  eupthf1o  16245  bj-charfunbi  16342  bj-inf2vnlem1  16501  pwf1oexmid  16536  subctctexmid  16537  iooref1o  16574  taupi  16613  alsi2d  16622  alsc2d  16624