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  11110  caucvgre  11234  cvg1nlemcau  11237  cvg1nlemres  11238  resqrexlemoverl  11274  sqrtge0  11286  fimaxre2  11480  climi  11540  reccn2ap  11566  climge0  11578  nnf1o  11629  sumpr  11666  fsump1i  11686  fsum00  11715  fsumparts  11723  mertenslemi1  11788  addsin  11995  subsin  11996  addcos  11999  subcos  12000  sinbnd2  12007  cosbnd2  12008  sinltxirr  12014  dvdsaddre2b  12094  evenelz  12120  4dvdseven  12170  gcd0id  12242  gcd1  12250  bezoutlemstep  12260  dvdsgcdb  12276  mulgcd  12279  gcdzeq  12285  dvdsmulgcd  12288  sqgcd  12292  dvdssqlem  12293  bezoutr  12295  uzwodc  12300  nninfctlemfo  12303  lcmval  12327  lcmcllem  12331  lcmgcdlem  12341  lcmdvds  12343  lcmgcdeq  12347  lcmdvdsb  12348  mulgcddvds  12358  rpmulgcd2  12359  qredeu  12361  rpdvds  12363  divgcdcoprm0  12365  isprm3  12382  divgcdodd  12407  coprm  12408  rpexp  12417  sqrt2irr  12426  qdencl  12453  qeqnumdivden  12458  divnumden  12460  divdenle  12461  densq  12468  phimullem  12489  eulerthlem1  12491  eulerthlemrprm  12493  eulerthlemth  12496  prmdiveq  12500  prmdivdiv  12501  hashgcdeq  12504  phisum  12505  odzid  12509  reumodprminv  12518  oddn2prm  12526  pythagtriplem4  12533  pythagtriplem11  12539  pythagtriplem13  12541  pythagtriplem19  12547  pclemub  12552  pcprendvds2  12556  pcpre1  12557  pcpremul  12558  pceulem  12559  pczdvds  12579  pc2dvds  12595  pcaddlem  12604  pcmpt  12608  pcmpt2  12609  pcmptdvds  12610  pcprod  12611  pockthlem  12621  pockthg  12622  prmunb  12627  1arithlem4  12631  4sqlem7  12649  4sqlem8  12650  4sqlem9  12651  4sqlem10  12652  4sqlemffi  12661  4sqlem15  12670  4sqlem16  12671  4sqlem17  12672  4sqlem18  12673  ennnfonelemom  12721  ennnfonelemex  12727  ennnfonelemf1  12731  ctiunctlemu1st  12747  ctiunctlemu2nd  12748  fnpr2ob  13114  mgmlrid  13153  gsumfzval  13165  gsumval2  13171  mndrid  13210  prdsmndd  13222  grpinvcnv  13342  dfgrp3mlem  13372  prdsgrpd  13383  prdsinvgd  13384  eqglact  13503  ghmgrp2  13524  ghmlin  13526  ghmnsgpreima  13547  kerf1ghm  13552  srgdilem  13673  srgdir  13679  srgridm  13684  ringdilem  13716  ringdir  13723  ringridm  13728  unitmulcl  13817  unitnegcl  13834  rhmmhm  13863  elrhmunit  13881  lringuplu  13900  subrgring  13928  subrg1cl  13933  qusrhm  14232  znunit  14363  znrrg  14364  psrelbas  14379  mplsubgfilemcl  14403  mplsubgfileminv  14404  inopn  14417  restbasg  14582  ssrest  14596  cntop2  14616  icnpimaex  14625  cnima  14634  lmfss  14658  lmtopcnp  14664  txhmeo  14733  txswaphmeo  14735  psmet0  14741  psmettri2  14742  blhalf  14822  bdxmet  14915  xmetxpbl  14922  ioo2bl  14965  tgioo  14968  cncfi  14992  rescncf  14995  cdivcncfap  15018  cnopnap  15025  divcncfap  15028  dedekindeulemeu  15036  dedekindicclemeu  15045  ivthinclemum  15049  ivthinclemlopn  15050  ivthinclemuopn  15052  ivthinclemdisj  15054  ivthdec  15058  ivthreinc  15059  limcimo  15079  cnplimcim  15081  cnplimclemr  15083  cnlimci  15087  limccnpcntop  15089  limccnp2lem  15090  limccnp2cntop  15091  limccoap  15092  reldvg  15093  dvbsssg  15100  dvfgg  15102  dvaddxxbr  15115  dvmulxxbr  15116  dvcoapbr  15121  dvcjbr  15122  dvrecap  15127  plyco  15173  plycj  15175  plyrecj  15177  sin0pilem1  15195  sin0pilem2  15196  tanrpcl  15251  tangtx  15252  cos0pilt1  15266  logbgcd1irraplemexp  15382  mpodvdsmulf1o  15404  perfect  15415  lgsne0  15457  lgseisen  15493  lgsquad2lem2  15501  2sqlem8a  15541  2sqlem8  15542  structgrssiedg  15582  bj-charfunbi  15680  bj-inf2vnlem1  15839  pwf1oexmid  15869  subctctexmid  15870  iooref1o  15906  taupi  15945  alsi2d  15954  alsc2d  15956