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  4235  potr  4306  frind  4350  brrelex2  4665  funinsn  5262  feu  5395  fcnvres  5396  fun11iun  5479  elmpocl2  6066  oprssdmm  6167  tfrlem1  6304  tfrlemisucfn  6320  tfrlemisucaccv  6321  tfrlemibxssdm  6323  tfrlemibfn  6324  tfrlemi14d  6329  swoer  6558  elmapssres  6668  mapsspm  6677  pmsspw  6678  mapss  6686  dom0  6833  xpf1o  6839  sbthlemi8  6958  sbthlemi9  6959  supelti  6996  supisoti  7004  djulclb  7049  nnnninfeq2  7122  cardcl  7175  isnumi  7176  cardval3ex  7179  exmidonfinlem  7187  en2eleq  7189  acfun  7201  exmidaclem  7202  dftap2  7245  exmidapne  7254  ccfunen  7258  indpi  7336  dfplpq2  7348  ltbtwnnq  7410  enq0tr  7428  nqnq0pi  7432  elnp1st2nd  7470  prcunqu  7479  prnmaxl  7482  prloc  7485  genpcuu  7514  addnqprllem  7521  addlocprlemeq  7527  addlocprlemgt  7528  addlocpr  7530  nqprxx  7540  gtnqex  7544  appdivnq  7557  prmuloclemcalc  7559  prmuloc  7560  mullocprlem  7564  ltprordil  7583  ltnqpri  7588  ltexprlemm  7594  ltexprlemopl  7595  ltexprlemlol  7596  ltexprlemopu  7597  ltexprlemupu  7598  ltexprlemdisj  7600  ltexprlemloc  7601  ltexprlemfl  7603  ltexprlemrl  7604  ltexprlemfu  7605  ltexprlemru  7606  ltexpri  7607  recexprlemell  7616  recexprlemelu  7617  recexprlemloc  7625  recexprlempr  7626  recexprlem1ssl  7627  recexprlem1ssu  7628  recexprlemss1l  7629  aptipr  7635  cauappcvgprlemlol  7641  cauappcvgprlemupu  7643  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  cauappcvgprlemladdrl  7651  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemlol  7664  caucvgprlemupu  7666  caucvgprlemladdfu  7671  caucvgprlem1  7673  caucvgprlem2  7674  caucvgprprlemnjltk  7685  caucvgprprlemnbj  7687  caucvgprprlemlol  7692  caucvgprprlemupu  7694  caucvgprprlemexbt  7700  caucvgprprlem1  7703  caucvgprprlem2  7704  suplocexprlemrl  7711  suplocexprlemru  7713  suplocexprlemdisj  7714  suplocexprlemub  7717  suplocexprlemlub  7718  ltsrprg  7741  gt0srpr  7742  recexgt0sr  7767  addgt0sr  7769  mulgt0sr  7772  map2psrprg  7799  suplocsrlemb  7800  suplocsrlem  7802  nnindnn  7887  axcaucvglemcau  7892  axpre-suploclemres  7895  apreap  8538  apreim  8554  mulge0  8570  apti  8573  mulap0bbd  8611  lble  8898  nnind  8929  recnz  9340  uzind  9358  eluzadd  9550  eluzsub  9551  ixxss1  9898  ixxss2  9899  ixxss12  9900  iccss2  9938  iccssioo2  9940  iccssico2  9941  elfzolt2  10149  ioom  10254  elicore  10260  flqltp1  10272  addmodlteq  10391  expcl2lemap  10525  expap0i  10545  hashennnuni  10750  crre  10857  caucvgre  10981  cvg1nlemcau  10984  cvg1nlemres  10985  resqrexlemoverl  11021  sqrtge0  11033  fimaxre2  11226  climi  11286  reccn2ap  11312  climge0  11324  nnf1o  11375  sumpr  11412  fsump1i  11432  fsum00  11461  fsumparts  11469  mertenslemi1  11534  addsin  11741  subsin  11742  addcos  11745  subcos  11746  sinbnd2  11753  cosbnd2  11754  evenelz  11862  4dvdseven  11912  infssuzcldc  11942  gcd0id  11970  gcd1  11978  bezoutlemstep  11988  dvdsgcdb  12004  mulgcd  12007  gcdzeq  12013  dvdsmulgcd  12016  sqgcd  12020  dvdssqlem  12021  bezoutr  12023  uzwodc  12028  lcmval  12053  lcmcllem  12057  lcmgcdlem  12067  lcmdvds  12069  lcmgcdeq  12073  lcmdvdsb  12074  mulgcddvds  12084  rpmulgcd2  12085  qredeu  12087  rpdvds  12089  divgcdcoprm0  12091  isprm3  12108  divgcdodd  12133  coprm  12134  rpexp  12143  sqrt2irr  12152  qdencl  12179  qeqnumdivden  12184  divnumden  12186  divdenle  12187  densq  12194  phimullem  12215  eulerthlem1  12217  eulerthlemrprm  12219  eulerthlemth  12222  prmdiveq  12226  prmdivdiv  12227  hashgcdeq  12229  phisum  12230  odzid  12234  reumodprminv  12243  oddn2prm  12251  pythagtriplem4  12258  pythagtriplem11  12264  pythagtriplem13  12266  pythagtriplem19  12272  pclemub  12277  pcprendvds2  12281  pcpre1  12282  pcpremul  12283  pceulem  12284  pczdvds  12303  pc2dvds  12319  pcaddlem  12328  pcmpt  12331  pcmpt2  12332  pcmptdvds  12333  pcprod  12334  pockthlem  12344  pockthg  12345  prmunb  12350  1arithlem4  12354  4sqlem7  12372  4sqlem8  12373  4sqlem9  12374  4sqlem10  12375  ennnfonelemom  12399  ennnfonelemex  12405  ennnfonelemf1  12409  ctiunctlemu1st  12425  ctiunctlemu2nd  12426  mgmlrid  12728  mndrid  12767  grpinvcnv  12866  dfgrp3mlem  12896  srgdilem  13052  srgdir  13058  srgridm  13063  ringdilem  13095  ringdir  13102  ringridm  13107  unitmulcl  13181  unitnegcl  13198  lringuplu  13236  inopn  13283  restbasg  13450  ssrest  13464  cntop2  13484  icnpimaex  13493  cnima  13502  lmfss  13526  lmtopcnp  13532  txhmeo  13601  txswaphmeo  13603  psmet0  13609  psmettri2  13610  blhalf  13690  bdxmet  13783  xmetxpbl  13790  ioo2bl  13825  tgioo  13828  cncfi  13847  rescncf  13850  cdivcncfap  13869  cnopnap  13876  dedekindeulemeu  13882  dedekindicclemeu  13891  ivthinclemum  13895  ivthinclemlopn  13896  ivthinclemuopn  13898  ivthinclemdisj  13900  ivthdec  13904  limcimo  13916  cnplimcim  13918  cnplimclemr  13920  cnlimci  13924  limccnpcntop  13926  limccnp2lem  13927  limccnp2cntop  13928  limccoap  13929  reldvg  13930  dvbsssg  13937  dvfgg  13939  dvaddxxbr  13947  dvmulxxbr  13948  dvcoapbr  13953  dvcjbr  13954  dvrecap  13959  sin0pilem1  13984  sin0pilem2  13985  tanrpcl  14040  tangtx  14041  cos0pilt1  14055  logbgcd1irraplemexp  14168  lgsne0  14221  2sqlem8a  14240  2sqlem8  14241  bj-charfunbi  14334  bj-inf2vnlem1  14493  pwf1oexmid  14520  subctctexmid  14521  iooref1o  14553  taupi  14591  alsi2d  14600  alsc2d  14602