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  3209  unssbd  3382  opth  4322  potr  4398  frind  4442  brrelex2  4759  funinsn  5369  feu  5507  fcnvres  5508  fun11iun  5592  funopsn  5816  elmpocl2  6201  uchoice  6281  oprssdmm  6315  tfrlem1  6452  tfrlemisucfn  6468  tfrlemisucaccv  6469  tfrlemibxssdm  6471  tfrlemibfn  6472  tfrlemi14d  6477  swoer  6706  elmapssres  6818  mapsspm  6827  pmsspw  6828  mapss  6836  dom0  6995  xpf1o  7001  sbthlemi8  7127  sbthlemi9  7128  supelti  7165  supisoti  7173  djulclb  7218  nninfninc  7286  nnnninfeq2  7292  cardcl  7349  isnumi  7350  cardval3ex  7353  exmidonfinlem  7367  en2eleq  7369  finacn  7382  acfun  7385  exmidaclem  7386  pw1if  7406  dftap2  7433  exmidapne  7442  ccfunen  7446  acnccim  7454  indpi  7525  dfplpq2  7537  ltbtwnnq  7599  enq0tr  7617  nqnq0pi  7621  elnp1st2nd  7659  prcunqu  7668  prnmaxl  7671  prloc  7674  genpcuu  7703  addnqprllem  7710  addlocprlemeq  7716  addlocprlemgt  7717  addlocpr  7719  nqprxx  7729  gtnqex  7733  appdivnq  7746  prmuloclemcalc  7748  prmuloc  7749  mullocprlem  7753  ltprordil  7772  ltnqpri  7777  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  ltexprlemdisj  7789  ltexprlemloc  7790  ltexprlemfl  7792  ltexprlemrl  7793  ltexprlemfu  7794  ltexprlemru  7795  ltexpri  7796  recexprlemell  7805  recexprlemelu  7806  recexprlemloc  7814  recexprlempr  7815  recexprlem1ssl  7816  recexprlem1ssu  7817  recexprlemss1l  7818  aptipr  7824  cauappcvgprlemlol  7830  cauappcvgprlemupu  7832  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdrl  7840  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemlol  7853  caucvgprlemupu  7855  caucvgprlemladdfu  7860  caucvgprlem1  7862  caucvgprlem2  7863  caucvgprprlemnjltk  7874  caucvgprprlemnbj  7876  caucvgprprlemlol  7881  caucvgprprlemupu  7883  caucvgprprlemexbt  7889  caucvgprprlem1  7892  caucvgprprlem2  7893  suplocexprlemrl  7900  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemub  7906  suplocexprlemlub  7907  ltsrprg  7930  gt0srpr  7931  recexgt0sr  7956  addgt0sr  7958  mulgt0sr  7961  map2psrprg  7988  suplocsrlemb  7989  suplocsrlem  7991  nnindnn  8076  axcaucvglemcau  8081  axpre-suploclemres  8084  apreap  8730  apreim  8746  mulge0  8762  apti  8765  mulap0bbd  8803  lble  9090  nnind  9122  recnz  9536  uzind  9554  eluzadd  9747  eluzsub  9748  ixxss1  10096  ixxss2  10097  ixxss12  10098  iccss2  10136  iccssioo2  10138  iccssico2  10139  elfzolt2  10349  infssuzcldc  10450  ioom  10475  elicore  10481  flqltp1  10494  addmodlteq  10615  expcl2lemap  10768  expap0i  10788  hashennnuni  10996  hashdmprop2dom  11061  wrdexb  11078  swrdsbslen  11193  swrdspsleq  11194  crre  11363  caucvgre  11487  cvg1nlemcau  11490  cvg1nlemres  11491  resqrexlemoverl  11527  sqrtge0  11539  fimaxre2  11733  climi  11793  reccn2ap  11819  climge0  11831  nnf1o  11882  sumpr  11919  fsump1i  11939  fsum00  11968  fsumparts  11976  mertenslemi1  12041  addsin  12248  subsin  12249  addcos  12252  subcos  12253  sinbnd2  12260  cosbnd2  12261  sinltxirr  12267  dvdsaddre2b  12347  evenelz  12373  4dvdseven  12423  gcd0id  12495  gcd1  12503  bezoutlemstep  12513  dvdsgcdb  12529  mulgcd  12532  gcdzeq  12538  dvdsmulgcd  12541  sqgcd  12545  dvdssqlem  12546  bezoutr  12548  uzwodc  12553  nninfctlemfo  12556  lcmval  12580  lcmcllem  12584  lcmgcdlem  12594  lcmdvds  12596  lcmgcdeq  12600  lcmdvdsb  12601  mulgcddvds  12611  rpmulgcd2  12612  qredeu  12614  rpdvds  12616  divgcdcoprm0  12618  isprm3  12635  divgcdodd  12660  coprm  12661  rpexp  12670  sqrt2irr  12679  qdencl  12706  qeqnumdivden  12711  divnumden  12713  divdenle  12714  densq  12721  phimullem  12742  eulerthlem1  12744  eulerthlemrprm  12746  eulerthlemth  12749  prmdiveq  12753  prmdivdiv  12754  hashgcdeq  12757  phisum  12758  odzid  12762  reumodprminv  12771  oddn2prm  12779  pythagtriplem4  12786  pythagtriplem11  12792  pythagtriplem13  12794  pythagtriplem19  12800  pclemub  12805  pcprendvds2  12809  pcpre1  12810  pcpremul  12811  pceulem  12812  pczdvds  12832  pc2dvds  12848  pcaddlem  12857  pcmpt  12861  pcmpt2  12862  pcmptdvds  12863  pcprod  12864  pockthlem  12874  pockthg  12875  prmunb  12880  1arithlem4  12884  4sqlem7  12902  4sqlem8  12903  4sqlem9  12904  4sqlem10  12905  4sqlemffi  12914  4sqlem15  12923  4sqlem16  12924  4sqlem17  12925  4sqlem18  12926  ennnfonelemom  12974  ennnfonelemex  12980  ennnfonelemf1  12984  ctiunctlemu1st  13000  ctiunctlemu2nd  13001  fnpr2ob  13368  mgmlrid  13407  gsumfzval  13419  gsumval2  13425  mndrid  13464  prdsmndd  13476  grpinvcnv  13596  dfgrp3mlem  13626  prdsgrpd  13637  prdsinvgd  13638  eqglact  13757  ghmgrp2  13778  ghmlin  13780  ghmnsgpreima  13801  kerf1ghm  13806  srgdilem  13927  srgdir  13933  srgridm  13938  ringdilem  13970  ringdir  13977  ringridm  13982  unitmulcl  14071  unitnegcl  14088  rhmmhm  14117  elrhmunit  14135  lringuplu  14154  subrgring  14182  subrg1cl  14187  qusrhm  14486  znunit  14617  znrrg  14618  psrelbas  14633  mplsubgfilemcl  14657  mplsubgfileminv  14658  inopn  14671  restbasg  14836  ssrest  14850  cntop2  14870  icnpimaex  14879  cnima  14888  lmfss  14912  lmtopcnp  14918  txhmeo  14987  txswaphmeo  14989  psmet0  14995  psmettri2  14996  blhalf  15076  bdxmet  15169  xmetxpbl  15176  ioo2bl  15219  tgioo  15222  cncfi  15246  rescncf  15249  cdivcncfap  15272  cnopnap  15279  divcncfap  15282  dedekindeulemeu  15290  dedekindicclemeu  15299  ivthinclemum  15303  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthinclemdisj  15308  ivthdec  15312  ivthreinc  15313  limcimo  15333  cnplimcim  15335  cnplimclemr  15337  cnlimci  15341  limccnpcntop  15343  limccnp2lem  15344  limccnp2cntop  15345  limccoap  15346  reldvg  15347  dvbsssg  15354  dvfgg  15356  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcjbr  15376  dvrecap  15381  plyco  15427  plycj  15429  plyrecj  15431  sin0pilem1  15449  sin0pilem2  15450  tanrpcl  15505  tangtx  15506  cos0pilt1  15520  logbgcd1irraplemexp  15636  mpodvdsmulf1o  15658  perfect  15669  lgsne0  15711  lgseisen  15747  lgsquad2lem2  15755  2sqlem8a  15795  2sqlem8  15796  structgrssiedg  15838  uhgrm  15872  umgredgne  15942  usgruspgrben  15978  usgredgppren  15989  umgr2edg  15999  wlkpropg  16030  wlkvtxeledgg  16041  bj-charfunbi  16132  bj-inf2vnlem1  16291  pwf1oexmid  16324  subctctexmid  16325  iooref1o  16361  taupi  16400  alsi2d  16409  alsc2d  16411