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  1774  eldifbd  3139  unssbd  3311  opth  4231  potr  4302  frind  4346  brrelex2  4661  funinsn  5257  feu  5390  fcnvres  5391  fun11iun  5474  elmpocl2  6061  oprssdmm  6162  tfrlem1  6299  tfrlemisucfn  6315  tfrlemisucaccv  6316  tfrlemibxssdm  6318  tfrlemibfn  6319  tfrlemi14d  6324  swoer  6553  elmapssres  6663  mapsspm  6672  pmsspw  6673  mapss  6681  dom0  6828  xpf1o  6834  sbthlemi8  6953  sbthlemi9  6954  supelti  6991  supisoti  6999  djulclb  7044  nnnninfeq2  7117  cardcl  7170  isnumi  7171  cardval3ex  7174  exmidonfinlem  7182  en2eleq  7184  acfun  7196  exmidaclem  7197  ccfunen  7238  indpi  7316  dfplpq2  7328  ltbtwnnq  7390  enq0tr  7408  nqnq0pi  7412  elnp1st2nd  7450  prcunqu  7459  prnmaxl  7462  prloc  7465  genpcuu  7494  addnqprllem  7501  addlocprlemeq  7507  addlocprlemgt  7508  addlocpr  7510  nqprxx  7520  gtnqex  7524  appdivnq  7537  prmuloclemcalc  7539  prmuloc  7540  mullocprlem  7544  ltprordil  7563  ltnqpri  7568  ltexprlemm  7574  ltexprlemopl  7575  ltexprlemlol  7576  ltexprlemopu  7577  ltexprlemupu  7578  ltexprlemdisj  7580  ltexprlemloc  7581  ltexprlemfl  7583  ltexprlemrl  7584  ltexprlemfu  7585  ltexprlemru  7586  ltexpri  7587  recexprlemell  7596  recexprlemelu  7597  recexprlemloc  7605  recexprlempr  7606  recexprlem1ssl  7607  recexprlem1ssu  7608  recexprlemss1l  7609  aptipr  7615  cauappcvgprlemlol  7621  cauappcvgprlemupu  7623  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  cauappcvgprlemladdrl  7631  caucvgprlemnkj  7640  caucvgprlemnbj  7641  caucvgprlemlol  7644  caucvgprlemupu  7646  caucvgprlemladdfu  7651  caucvgprlem1  7653  caucvgprlem2  7654  caucvgprprlemnjltk  7665  caucvgprprlemnbj  7667  caucvgprprlemlol  7672  caucvgprprlemupu  7674  caucvgprprlemexbt  7680  caucvgprprlem1  7683  caucvgprprlem2  7684  suplocexprlemrl  7691  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemub  7697  suplocexprlemlub  7698  ltsrprg  7721  gt0srpr  7722  recexgt0sr  7747  addgt0sr  7749  mulgt0sr  7752  map2psrprg  7779  suplocsrlemb  7780  suplocsrlem  7782  nnindnn  7867  axcaucvglemcau  7872  axpre-suploclemres  7875  apreap  8518  apreim  8534  mulge0  8550  apti  8553  mulap0bbd  8590  lble  8875  nnind  8906  recnz  9317  uzind  9335  eluzadd  9527  eluzsub  9528  ixxss1  9873  ixxss2  9874  ixxss12  9875  iccss2  9913  iccssioo2  9915  iccssico2  9916  elfzolt2  10124  ioom  10229  elicore  10235  flqltp1  10247  addmodlteq  10366  expcl2lemap  10500  expap0i  10520  hashennnuni  10725  crre  10832  caucvgre  10956  cvg1nlemcau  10959  cvg1nlemres  10960  resqrexlemoverl  10996  sqrtge0  11008  fimaxre2  11201  climi  11261  reccn2ap  11287  climge0  11299  nnf1o  11350  sumpr  11387  fsump1i  11407  fsum00  11436  fsumparts  11444  mertenslemi1  11509  addsin  11716  subsin  11717  addcos  11720  subcos  11721  sinbnd2  11728  cosbnd2  11729  evenelz  11837  4dvdseven  11887  infssuzcldc  11917  gcd0id  11945  gcd1  11953  bezoutlemstep  11963  dvdsgcdb  11979  mulgcd  11982  gcdzeq  11988  dvdsmulgcd  11991  sqgcd  11995  dvdssqlem  11996  bezoutr  11998  uzwodc  12003  lcmval  12028  lcmcllem  12032  lcmgcdlem  12042  lcmdvds  12044  lcmgcdeq  12048  lcmdvdsb  12049  mulgcddvds  12059  rpmulgcd2  12060  qredeu  12062  rpdvds  12064  divgcdcoprm0  12066  isprm3  12083  divgcdodd  12108  coprm  12109  rpexp  12118  sqrt2irr  12127  qdencl  12154  qeqnumdivden  12159  divnumden  12161  divdenle  12162  densq  12169  phimullem  12190  eulerthlem1  12192  eulerthlemrprm  12194  eulerthlemth  12197  prmdiveq  12201  prmdivdiv  12202  hashgcdeq  12204  phisum  12205  odzid  12209  reumodprminv  12218  oddn2prm  12226  pythagtriplem4  12233  pythagtriplem11  12239  pythagtriplem13  12241  pythagtriplem19  12247  pclemub  12252  pcprendvds2  12256  pcpre1  12257  pcpremul  12258  pceulem  12259  pczdvds  12278  pc2dvds  12294  pcaddlem  12303  pcmpt  12306  pcmpt2  12307  pcmptdvds  12308  pcprod  12309  pockthlem  12319  pockthg  12320  prmunb  12325  1arithlem4  12329  4sqlem7  12347  4sqlem8  12348  4sqlem9  12349  4sqlem10  12350  ennnfonelemom  12374  ennnfonelemex  12380  ennnfonelemf1  12384  ctiunctlemu1st  12400  ctiunctlemu2nd  12401  mgmlrid  12662  mndrid  12701  grpinvcnv  12797  dfgrp3mlem  12827  srgdilem  12945  srgdir  12951  srgridm  12956  ringdilem  12988  ringdir  12995  ringridm  13000  inopn  13052  restbasg  13219  ssrest  13233  cntop2  13253  icnpimaex  13262  cnima  13271  lmfss  13295  lmtopcnp  13301  txhmeo  13370  txswaphmeo  13372  psmet0  13378  psmettri2  13379  blhalf  13459  bdxmet  13552  xmetxpbl  13559  ioo2bl  13594  tgioo  13597  cncfi  13616  rescncf  13619  cdivcncfap  13638  cnopnap  13645  dedekindeulemeu  13651  dedekindicclemeu  13660  ivthinclemum  13664  ivthinclemlopn  13665  ivthinclemuopn  13667  ivthinclemdisj  13669  ivthdec  13673  limcimo  13685  cnplimcim  13687  cnplimclemr  13689  cnlimci  13693  limccnpcntop  13695  limccnp2lem  13696  limccnp2cntop  13697  limccoap  13698  reldvg  13699  dvbsssg  13706  dvfgg  13708  dvaddxxbr  13716  dvmulxxbr  13717  dvcoapbr  13722  dvcjbr  13723  dvrecap  13728  sin0pilem1  13753  sin0pilem2  13754  tanrpcl  13809  tangtx  13810  cos0pilt1  13824  logbgcd1irraplemexp  13937  lgsne0  13990  2sqlem8a  14009  2sqlem8  14010  bj-charfunbi  14103  bj-inf2vnlem1  14262  pwf1oexmid  14289  subctctexmid  14291  iooref1o  14323  taupi  14359  alsi2d  14368  alsc2d  14370