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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107

This theorem is used by:  biimpr  130  simprbi  275  simplbda  384  simplrd  534  simprld  536  simprrd  538  simp2  1029  simp3  1030  sbh  1829  eldifbd  3232  unssbd  3407  opth  4377  potr  4453  frind  4497  brrelex2  4816  funinsn  5430  feu  5574  fcnvres  5575  fun11iun  5660  funopsn  5891  elmpocl2  6286  uchoice  6371  oprssdmm  6405  fczsupp0  6499  tfrlem1  6579  tfrlemisucfn  6595  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi14d  6604  swoer  6835  elmapssres  6954  mapsspm  6963  pmsspw  6964  mapss  6973  dom0  7138  xpf1o  7144  sbthlemi8  7281  sbthlemi9  7282  fsuppimpd  7293  supelti  7343  supisoti  7351  djulclb  7396  nninfninc  7464  nnnninfeq2  7470  cardcl  7527  isnumi  7528  cardval3ex  7531  exmidonfinlem  7546  en2eleq  7548  finacn  7561  acfun  7564  exmidaclem  7565  pw1if  7585  papirr  7612  dftap2  7618  exmidapne  7627  ccfunen  7631  acnccim  7639  indpi  7710  dfplpq2  7722  ltbtwnnq  7784  enq0tr  7802  nqnq0pi  7806  elnp1st2nd  7844  prcunqu  7853  prnmaxl  7856  prloc  7859  genpcuu  7888  addnqprllem  7895  addlocprlemeq  7901  addlocprlemgt  7902  addlocpr  7904  nqprxx  7914  gtnqex  7918  appdivnq  7931  prmuloclemcalc  7933  prmuloc  7934  mullocprlem  7938  ltprordil  7957  ltnqpri  7962  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  ltexpri  7981  recexprlemell  7990  recexprlemelu  7991  recexprlemloc  7999  recexprlempr  8000  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  aptipr  8009  cauappcvgprlemlol  8015  cauappcvgprlemupu  8017  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdrl  8025  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemlol  8038  caucvgprlemupu  8040  caucvgprlemladdfu  8045  caucvgprlem1  8047  caucvgprlem2  8048  caucvgprprlemnjltk  8059  caucvgprprlemnbj  8061  caucvgprprlemlol  8066  caucvgprprlemupu  8068  caucvgprprlemexbt  8074  caucvgprprlem1  8077  caucvgprprlem2  8078  suplocexprlemrl  8085  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemub  8091  suplocexprlemlub  8092  ltsrprg  8115  gt0srpr  8116  recexgt0sr  8141  addgt0sr  8143  mulgt0sr  8146  map2psrprg  8173  suplocsrlemb  8174  suplocsrlem  8176  nnindnn  8261  axcaucvglemcau  8266  axpre-suploclemres  8269  apreap  8918  apreim  8934  mulge0  8950  apti  8953  mulap0bbd  8991  lble  9280  nnind  9323  recnz  9744  uzind  9762  eluzadd  9961  eluzsub  9962  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  iccssioo2  10359  iccssico2  10360  elfzolt2  10575  infssuzcldc  10679  ioom  10706  elicore  10712  flqltp1  10727  flapge  10731  flaplt  10733  addmodlteq  10850  expcl2lemap  11003  expap0i  11023  hashennnuni  11234  hashf1lem2  11302  hashdmprop2dom  11312  wrdexb  11332  swrdsbslen  11454  swrdspsleq  11455  crre  11638  sq01  11676  caucvgre  11763  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemoverl  11803  sqrtge0  11815  fimaxre2  12010  climi  12072  reccn2ap  12098  climge0  12110  nnf1o  12162  sumpr  12199  fsump1i  12219  fsum00  12248  fsumparts  12256  mertenslemi1  12321  addsin  12528  subsin  12529  addcos  12532  subcos  12533  sinbnd2  12540  cosbnd2  12541  sinltxirr  12547  dvdsaddre2b  12627  evenelz  12653  4dvdseven  12703  gcd0id  12775  gcd1  12783  bezoutlemstep  12793  dvdsgcdb  12809  mulgcd  12812  gcdzeq  12818  dvdsmulgcd  12821  sqgcd  12825  dvdssqlem  12826  bezoutr  12828  uzwodc  12833  nninfctlemfo  12836  lcmval  12860  lcmcllem  12864  lcmgcdlem  12874  lcmdvds  12876  lcmgcdeq  12880  lcmdvdsb  12881  mulgcddvds  12891  rpmulgcd2  12892  qredeu  12894  rpdvds  12896  divgcdcoprm0  12898  isprm3  12915  divgcdodd  12941  coprm  12942  rpexp  12951  sqrt2irr  12960  qdencl  12988  qeqnumdivden  12993  divnumden  12995  divdenle  12996  densq  13003  phimullem  13026  eulerthlem1  13028  eulerthlemrprm  13030  eulerthlemth  13033  prmdiveq  13037  prmdivdiv  13038  hashgcdeq  13041  phisum  13042  odzid  13046  reumodprminv  13055  oddn2prm  13063  pythagtriplem4  13070  pythagtriplem11  13076  pythagtriplem13  13078  pythagtriplem19  13084  pclemub  13089  pcprendvds2  13093  pcpre1  13094  pcpremul  13095  pceulem  13096  pczdvds  13116  pc2dvds  13132  pcaddlem  13141  pcmpt  13145  pcmpt2  13146  pcmptdvds  13147  pcprod  13148  pockthlem  13158  pockthg  13159  prmunb  13164  1arithlem4  13168  4sqlem7  13186  4sqlem8  13187  4sqlem9  13188  4sqlem10  13189  4sqlemffi  13198  4sqlem15  13207  4sqlem16  13208  4sqlem17  13209  4sqlem18  13210  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsf1o  13309  ballotfilemscr  13314  ballotfilemrv  13315  ballotfilemfrci  13323  ballotfilemfrceq  13324  ballotfilemrinv0  13328  ennnfonelemom  13351  ennnfonelemex  13357  ennnfonelemf1  13361  ctiunctlemu1st  13377  ctiunctlemu2nd  13378  fnpr2ob  13714  mgmlrid  13752  gzsumfzval  13764  gzsumval2  13767  mndrid  13802  grpinvcnv  13926  dfgrp3mlem  13956  eqglact  14081  ghmgrp2  14102  ghmlin  14104  ghmnsgpreima  14125  kerf1ghm  14130  resscntz  14160  cntzmhm  14167  gzsumsplit0  14232  prdsmndd  14278  prdsgrpd  14281  prdsinvgd  14282  srgdilem  14357  srgdir  14363  srgridm  14368  ringdilem  14400  ringdir  14408  ringridm  14413  unitmulcl  14504  unitnegcl  14521  rhmmhm  14550  elrhmunit  14568  lringuplu  14587  subrgring  14616  subrg1cl  14621  qusrhm  14949  znunit  15078  znrrg  15079  assaassr  15089  assaring  15091  psrbagfsupp  15139  psrbaglecl  15144  psrbagcon  15146  psrbagconcl  15148  psrelbas  15151  mplsubgfilemcl  15181  mplsubgfileminv  15182  inopn  15195  restbasg  15360  ssrest  15374  cntop2  15394  icnpimaex  15403  cnima  15412  lmfss  15436  lmtopcnp  15442  txhmeo  15511  txswaphmeo  15513  psmet0  15519  psmettri2  15520  blhalf  15600  bdxmet  15693  xmetxpbl  15700  ioo2bl  15743  tgioo  15746  cncfi  15770  rescncf  15773  cdivcncfap  15796  cnopnap  15803  divcncfap  15806  dedekindeulemeu  15814  dedekindicclemeu  15823  ivthinclemum  15827  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthinclemdisj  15832  ivthdec  15836  ivthreinc  15837  limcimo  15857  cnplimcim  15859  cnplimclemr  15861  cnlimci  15865  limccnpcntop  15867  limccnp2lem  15868  limccnp2cntop  15869  limccoap  15870  reldvg  15871  dvbsssg  15878  dvfgg  15880  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvrecap  15905  plyco  15951  plycj  15953  plyrecj  15955  sin0pilem1  15974  sin0pilem2  15975  tanrpcl  16030  tangtx  16031  cos0pilt1  16045  logbgcd1irraplemexp  16165  zprmlogbaplem2  16177  zprmlogbaplem3  16178  ppiqsval2  16202  chtqge0  16208  chtqwordi  16224  mpodvdsmulf1o  16245  perfect  16262  bposlem3  16274  bposlem5  16276  bposlem6  16277  bposlem9  16280  lgsne0  16323  lgseisen  16359  lgsquad2lem2  16367  2sqlem8a  16407  2sqlem8  16408  structgrssiedg  16450  uhgrm  16485  umgredgne  16557  usgruspgrben  16593  usgredgppren  16604  umgr2edg  16614  vtxdumgrfival  16705  wlkpropg  16731  wlkv  16733  wlkvtxeledgg  16751  g0wlk0  16777  trlsv  16791  clwwlknlen  16818  eupthv  16853  eupthf1o  16857  eupth2lem3lem4fi  16880  eulerpathprum  16887  bj-charfunbi  17003  bj-inf2vnlem1  17162  pwf1oexmid  17195  subctctexmid  17196  iooref1o  17249  taupi  17290  als2d  17301  rals2d  17303  alseu2d  17337  ralseu2d  17339