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  simplrd  534  simprld  536  simprrd  538  simp2  1029  simp3  1030  sbh  1829  eldifbd  3232  unssbd  3407  opth  4372  potr  4448  frind  4492  brrelex2  4811  funinsn  5425  feu  5569  fcnvres  5570  fun11iun  5655  funopsn  5882  elmpocl2  6276  uchoice  6361  oprssdmm  6395  fczsupp0  6489  tfrlem1  6569  tfrlemisucfn  6585  tfrlemisucaccv  6586  tfrlemibxssdm  6588  tfrlemibfn  6589  tfrlemi14d  6594  swoer  6825  elmapssres  6944  mapsspm  6953  pmsspw  6954  mapss  6963  dom0  7128  xpf1o  7134  sbthlemi8  7271  sbthlemi9  7272  fsuppimpd  7283  supelti  7332  supisoti  7340  djulclb  7385  nninfninc  7453  nnnninfeq2  7459  cardcl  7516  isnumi  7517  cardval3ex  7520  exmidonfinlem  7535  en2eleq  7537  finacn  7550  acfun  7553  exmidaclem  7554  pw1if  7574  papirr  7601  dftap2  7607  exmidapne  7616  ccfunen  7620  acnccim  7628  indpi  7699  dfplpq2  7711  ltbtwnnq  7773  enq0tr  7791  nqnq0pi  7795  elnp1st2nd  7833  prcunqu  7842  prnmaxl  7845  prloc  7848  genpcuu  7877  addnqprllem  7884  addlocprlemeq  7890  addlocprlemgt  7891  addlocpr  7893  nqprxx  7903  gtnqex  7907  appdivnq  7920  prmuloclemcalc  7922  prmuloc  7923  mullocprlem  7927  ltprordil  7946  ltnqpri  7951  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemlol  7959  ltexprlemopu  7960  ltexprlemupu  7961  ltexprlemdisj  7963  ltexprlemloc  7964  ltexprlemfl  7966  ltexprlemrl  7967  ltexprlemfu  7968  ltexprlemru  7969  ltexpri  7970  recexprlemell  7979  recexprlemelu  7980  recexprlemloc  7988  recexprlempr  7989  recexprlem1ssl  7990  recexprlem1ssu  7991  recexprlemss1l  7992  aptipr  7998  cauappcvgprlemlol  8004  cauappcvgprlemupu  8006  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdrl  8014  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemlol  8027  caucvgprlemupu  8029  caucvgprlemladdfu  8034  caucvgprlem1  8036  caucvgprlem2  8037  caucvgprprlemnjltk  8048  caucvgprprlemnbj  8050  caucvgprprlemlol  8055  caucvgprprlemupu  8057  caucvgprprlemexbt  8063  caucvgprprlem1  8066  caucvgprprlem2  8067  suplocexprlemrl  8074  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemub  8080  suplocexprlemlub  8081  ltsrprg  8104  gt0srpr  8105  recexgt0sr  8130  addgt0sr  8132  mulgt0sr  8135  map2psrprg  8162  suplocsrlemb  8163  suplocsrlem  8165  nnindnn  8250  axcaucvglemcau  8255  axpre-suploclemres  8258  apreap  8905  apreim  8921  mulge0  8937  apti  8940  mulap0bbd  8978  lble  9267  nnind  9299  recnz  9718  uzind  9736  eluzadd  9930  eluzsub  9931  ixxss1  10285  ixxss2  10286  ixxss12  10287  iccss2  10325  iccssioo2  10327  iccssico2  10328  elfzolt2  10542  infssuzcldc  10646  ioom  10673  elicore  10679  flqltp1  10692  addmodlteq  10813  expcl2lemap  10966  expap0i  10986  hashennnuni  11196  hashf1lem2  11264  hashdmprop2dom  11274  wrdexb  11294  swrdsbslen  11416  swrdspsleq  11417  crre  11600  sq01  11638  caucvgre  11725  cvg1nlemcau  11728  cvg1nlemres  11729  resqrexlemoverl  11765  sqrtge0  11777  fimaxre2  11971  climi  12031  reccn2ap  12057  climge0  12069  nnf1o  12121  sumpr  12158  fsump1i  12178  fsum00  12207  fsumparts  12215  mertenslemi1  12280  addsin  12487  subsin  12488  addcos  12491  subcos  12492  sinbnd2  12499  cosbnd2  12500  sinltxirr  12506  dvdsaddre2b  12586  evenelz  12612  4dvdseven  12662  gcd0id  12734  gcd1  12742  bezoutlemstep  12752  dvdsgcdb  12768  mulgcd  12771  gcdzeq  12777  dvdsmulgcd  12780  sqgcd  12784  dvdssqlem  12785  bezoutr  12787  uzwodc  12792  nninfctlemfo  12795  lcmval  12819  lcmcllem  12823  lcmgcdlem  12833  lcmdvds  12835  lcmgcdeq  12839  lcmdvdsb  12840  mulgcddvds  12850  rpmulgcd2  12851  qredeu  12853  rpdvds  12855  divgcdcoprm0  12857  isprm3  12874  divgcdodd  12899  coprm  12900  rpexp  12909  sqrt2irr  12918  qdencl  12945  qeqnumdivden  12950  divnumden  12952  divdenle  12953  densq  12960  phimullem  12981  eulerthlem1  12983  eulerthlemrprm  12985  eulerthlemth  12988  prmdiveq  12992  prmdivdiv  12993  hashgcdeq  12996  phisum  12997  odzid  13001  reumodprminv  13010  oddn2prm  13018  pythagtriplem4  13025  pythagtriplem11  13031  pythagtriplem13  13033  pythagtriplem19  13039  pclemub  13044  pcprendvds2  13048  pcpre1  13049  pcpremul  13050  pceulem  13051  pczdvds  13071  pc2dvds  13087  pcaddlem  13096  pcmpt  13100  pcmpt2  13101  pcmptdvds  13102  pcprod  13103  pockthlem  13113  pockthg  13114  prmunb  13119  1arithlem4  13123  4sqlem7  13141  4sqlem8  13142  4sqlem9  13143  4sqlem10  13144  4sqlemffi  13153  4sqlem15  13162  4sqlem16  13163  4sqlem17  13164  4sqlem18  13165  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemsf1o  13235  ballotfilemscr  13240  ballotfilemrv  13241  ballotfilemfrci  13249  ballotfilemfrceq  13250  ballotfilemrinv0  13254  ennnfonelemom  13277  ennnfonelemex  13283  ennnfonelemf1  13287  ctiunctlemu1st  13303  ctiunctlemu2nd  13304  fnpr2ob  13638  mgmlrid  13676  gzsumfzval  13688  gzsumval2  13691  mndrid  13726  grpinvcnv  13850  dfgrp3mlem  13880  eqglact  14005  ghmgrp2  14026  ghmlin  14028  ghmnsgpreima  14049  kerf1ghm  14054  gzsumsplit0  14125  prdsmndd  14171  prdsgrpd  14174  prdsinvgd  14175  srgdilem  14247  srgdir  14253  srgridm  14258  ringdilem  14290  ringdir  14297  ringridm  14302  unitmulcl  14393  unitnegcl  14410  rhmmhm  14439  elrhmunit  14457  lringuplu  14476  subrgring  14505  subrg1cl  14510  qusrhm  14837  znunit  14966  znrrg  14967  psrbagfsupp  14978  psrbaglecl  14983  psrbagcon  14985  psrbagconcl  14986  psrelbas  14989  mplsubgfilemcl  15013  mplsubgfileminv  15014  inopn  15027  restbasg  15192  ssrest  15206  cntop2  15226  icnpimaex  15235  cnima  15244  lmfss  15268  lmtopcnp  15274  txhmeo  15343  txswaphmeo  15345  psmet0  15351  psmettri2  15352  blhalf  15432  bdxmet  15525  xmetxpbl  15532  ioo2bl  15575  tgioo  15578  cncfi  15602  rescncf  15605  cdivcncfap  15628  cnopnap  15635  divcncfap  15638  dedekindeulemeu  15646  dedekindicclemeu  15655  ivthinclemum  15659  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthinclemdisj  15664  ivthdec  15668  ivthreinc  15669  limcimo  15689  cnplimcim  15691  cnplimclemr  15693  cnlimci  15697  limccnpcntop  15699  limccnp2lem  15700  limccnp2cntop  15701  limccoap  15702  reldvg  15703  dvbsssg  15710  dvfgg  15712  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvrecap  15737  plyco  15783  plycj  15785  plyrecj  15787  sin0pilem1  15805  sin0pilem2  15806  tanrpcl  15861  tangtx  15862  cos0pilt1  15876  logbgcd1irraplemexp  15993  mpodvdsmulf1o  16018  perfect  16029  lgsne0  16071  lgseisen  16107  lgsquad2lem2  16115  2sqlem8a  16155  2sqlem8  16156  structgrssiedg  16198  uhgrm  16233  umgredgne  16305  usgruspgrben  16341  usgredgppren  16352  umgr2edg  16362  vtxdumgrfival  16453  wlkpropg  16479  wlkv  16481  wlkvtxeledgg  16499  g0wlk0  16525  trlsv  16539  clwwlknlen  16566  eupthv  16601  eupthf1o  16605  eupth2lem3lem4fi  16628  eulerpathprum  16635  bj-charfunbi  16751  bj-inf2vnlem1  16910  pwf1oexmid  16943  subctctexmid  16944  iooref1o  16988  taupi  17028  alsi2d  17037  alsc2d  17039