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  1790  eldifbd  3169  unssbd  3342  opth  4271  potr  4344  frind  4388  brrelex2  4705  funinsn  5308  feu  5443  fcnvres  5444  fun11iun  5528  elmpocl2  6124  uchoice  6204  oprssdmm  6238  tfrlem1  6375  tfrlemisucfn  6391  tfrlemisucaccv  6392  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemi14d  6400  swoer  6629  elmapssres  6741  mapsspm  6750  pmsspw  6751  mapss  6759  dom0  6908  xpf1o  6914  sbthlemi8  7039  sbthlemi9  7040  supelti  7077  supisoti  7085  djulclb  7130  nninfninc  7198  nnnninfeq2  7204  cardcl  7261  isnumi  7262  cardval3ex  7265  exmidonfinlem  7274  en2eleq  7276  finacn  7289  acfun  7292  exmidaclem  7293  dftap2  7336  exmidapne  7345  ccfunen  7349  acnccim  7357  indpi  7428  dfplpq2  7440  ltbtwnnq  7502  enq0tr  7520  nqnq0pi  7524  elnp1st2nd  7562  prcunqu  7571  prnmaxl  7574  prloc  7577  genpcuu  7606  addnqprllem  7613  addlocprlemeq  7619  addlocprlemgt  7620  addlocpr  7622  nqprxx  7632  gtnqex  7636  appdivnq  7649  prmuloclemcalc  7651  prmuloc  7652  mullocprlem  7656  ltprordil  7675  ltnqpri  7680  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  ltexpri  7699  recexprlemell  7708  recexprlemelu  7709  recexprlemloc  7717  recexprlempr  7718  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  aptipr  7727  cauappcvgprlemlol  7733  cauappcvgprlemupu  7735  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdrl  7743  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemlol  7756  caucvgprlemupu  7758  caucvgprlemladdfu  7763  caucvgprlem1  7765  caucvgprlem2  7766  caucvgprprlemnjltk  7777  caucvgprprlemnbj  7779  caucvgprprlemlol  7784  caucvgprprlemupu  7786  caucvgprprlemexbt  7792  caucvgprprlem1  7795  caucvgprprlem2  7796  suplocexprlemrl  7803  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemub  7809  suplocexprlemlub  7810  ltsrprg  7833  gt0srpr  7834  recexgt0sr  7859  addgt0sr  7861  mulgt0sr  7864  map2psrprg  7891  suplocsrlemb  7892  suplocsrlem  7894  nnindnn  7979  axcaucvglemcau  7984  axpre-suploclemres  7987  apreap  8633  apreim  8649  mulge0  8665  apti  8668  mulap0bbd  8706  lble  8993  nnind  9025  recnz  9438  uzind  9456  eluzadd  9649  eluzsub  9650  ixxss1  9998  ixxss2  9999  ixxss12  10000  iccss2  10038  iccssioo2  10040  iccssico2  10041  elfzolt2  10251  infssuzcldc  10344  ioom  10369  elicore  10375  flqltp1  10388  addmodlteq  10509  expcl2lemap  10662  expap0i  10682  hashennnuni  10890  wrdexb  10966  crre  11041  caucvgre  11165  cvg1nlemcau  11168  cvg1nlemres  11169  resqrexlemoverl  11205  sqrtge0  11217  fimaxre2  11411  climi  11471  reccn2ap  11497  climge0  11509  nnf1o  11560  sumpr  11597  fsump1i  11617  fsum00  11646  fsumparts  11654  mertenslemi1  11719  addsin  11926  subsin  11927  addcos  11930  subcos  11931  sinbnd2  11938  cosbnd2  11939  sinltxirr  11945  dvdsaddre2b  12025  evenelz  12051  4dvdseven  12101  gcd0id  12173  gcd1  12181  bezoutlemstep  12191  dvdsgcdb  12207  mulgcd  12210  gcdzeq  12216  dvdsmulgcd  12219  sqgcd  12223  dvdssqlem  12224  bezoutr  12226  uzwodc  12231  nninfctlemfo  12234  lcmval  12258  lcmcllem  12262  lcmgcdlem  12272  lcmdvds  12274  lcmgcdeq  12278  lcmdvdsb  12279  mulgcddvds  12289  rpmulgcd2  12290  qredeu  12292  rpdvds  12294  divgcdcoprm0  12296  isprm3  12313  divgcdodd  12338  coprm  12339  rpexp  12348  sqrt2irr  12357  qdencl  12384  qeqnumdivden  12389  divnumden  12391  divdenle  12392  densq  12399  phimullem  12420  eulerthlem1  12422  eulerthlemrprm  12424  eulerthlemth  12427  prmdiveq  12431  prmdivdiv  12432  hashgcdeq  12435  phisum  12436  odzid  12440  reumodprminv  12449  oddn2prm  12457  pythagtriplem4  12464  pythagtriplem11  12470  pythagtriplem13  12472  pythagtriplem19  12478  pclemub  12483  pcprendvds2  12487  pcpre1  12488  pcpremul  12489  pceulem  12490  pczdvds  12510  pc2dvds  12526  pcaddlem  12535  pcmpt  12539  pcmpt2  12540  pcmptdvds  12541  pcprod  12542  pockthlem  12552  pockthg  12553  prmunb  12558  1arithlem4  12562  4sqlem7  12580  4sqlem8  12581  4sqlem9  12582  4sqlem10  12583  4sqlemffi  12592  4sqlem15  12601  4sqlem16  12602  4sqlem17  12603  4sqlem18  12604  ennnfonelemom  12652  ennnfonelemex  12658  ennnfonelemf1  12662  ctiunctlemu1st  12678  ctiunctlemu2nd  12679  fnpr2ob  13044  mgmlrid  13083  gsumfzval  13095  gsumval2  13101  mndrid  13140  prdsmndd  13152  grpinvcnv  13272  dfgrp3mlem  13302  prdsgrpd  13313  prdsinvgd  13314  eqglact  13433  ghmgrp2  13454  ghmlin  13456  ghmnsgpreima  13477  kerf1ghm  13482  srgdilem  13603  srgdir  13609  srgridm  13614  ringdilem  13646  ringdir  13653  ringridm  13658  unitmulcl  13747  unitnegcl  13764  rhmmhm  13793  elrhmunit  13811  lringuplu  13830  subrgring  13858  subrg1cl  13863  qusrhm  14162  znunit  14293  znrrg  14294  psrelbas  14309  mplsubgfilemcl  14333  mplsubgfileminv  14334  inopn  14347  restbasg  14512  ssrest  14526  cntop2  14546  icnpimaex  14555  cnima  14564  lmfss  14588  lmtopcnp  14594  txhmeo  14663  txswaphmeo  14665  psmet0  14671  psmettri2  14672  blhalf  14752  bdxmet  14845  xmetxpbl  14852  ioo2bl  14895  tgioo  14898  cncfi  14922  rescncf  14925  cdivcncfap  14948  cnopnap  14955  divcncfap  14958  dedekindeulemeu  14966  dedekindicclemeu  14975  ivthinclemum  14979  ivthinclemlopn  14980  ivthinclemuopn  14982  ivthinclemdisj  14984  ivthdec  14988  ivthreinc  14989  limcimo  15009  cnplimcim  15011  cnplimclemr  15013  cnlimci  15017  limccnpcntop  15019  limccnp2lem  15020  limccnp2cntop  15021  limccoap  15022  reldvg  15023  dvbsssg  15030  dvfgg  15032  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvcjbr  15052  dvrecap  15057  plyco  15103  plycj  15105  plyrecj  15107  sin0pilem1  15125  sin0pilem2  15126  tanrpcl  15181  tangtx  15182  cos0pilt1  15196  logbgcd1irraplemexp  15312  mpodvdsmulf1o  15334  perfect  15345  lgsne0  15387  lgseisen  15423  lgsquad2lem2  15431  2sqlem8a  15471  2sqlem8  15472  bj-charfunbi  15565  bj-inf2vnlem1  15724  pwf1oexmid  15754  subctctexmid  15755  iooref1o  15791  taupi  15830  alsi2d  15839  alsc2d  15841