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  7342  supisoti  7350  djulclb  7395  nninfninc  7463  nnnninfeq2  7469  cardcl  7526  isnumi  7527  cardval3ex  7530  exmidonfinlem  7545  en2eleq  7547  finacn  7560  acfun  7563  exmidaclem  7564  pw1if  7584  papirr  7611  dftap2  7617  exmidapne  7626  ccfunen  7630  acnccim  7638  indpi  7709  dfplpq2  7721  ltbtwnnq  7783  enq0tr  7801  nqnq0pi  7805  elnp1st2nd  7843  prcunqu  7852  prnmaxl  7855  prloc  7858  genpcuu  7887  addnqprllem  7894  addlocprlemeq  7900  addlocprlemgt  7901  addlocpr  7903  nqprxx  7913  gtnqex  7917  appdivnq  7930  prmuloclemcalc  7932  prmuloc  7933  mullocprlem  7937  ltprordil  7956  ltnqpri  7961  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltexpri  7980  recexprlemell  7989  recexprlemelu  7990  recexprlemloc  7998  recexprlempr  7999  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  aptipr  8008  cauappcvgprlemlol  8014  cauappcvgprlemupu  8016  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdrl  8024  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemlol  8037  caucvgprlemupu  8039  caucvgprlemladdfu  8044  caucvgprlem1  8046  caucvgprlem2  8047  caucvgprprlemnjltk  8058  caucvgprprlemnbj  8060  caucvgprprlemlol  8065  caucvgprprlemupu  8067  caucvgprprlemexbt  8073  caucvgprprlem1  8076  caucvgprprlem2  8077  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemub  8090  suplocexprlemlub  8091  ltsrprg  8114  gt0srpr  8115  recexgt0sr  8140  addgt0sr  8142  mulgt0sr  8145  map2psrprg  8172  suplocsrlemb  8173  suplocsrlem  8175  nnindnn  8260  axcaucvglemcau  8265  axpre-suploclemres  8268  apreap  8917  apreim  8933  mulge0  8949  apti  8952  mulap0bbd  8990  lble  9279  nnind  9322  recnz  9743  uzind  9761  eluzadd  9960  eluzsub  9961  ixxss1  10316  ixxss2  10317  ixxss12  10318  iccss2  10356  iccssioo2  10358  iccssico2  10359  elfzolt2  10574  infssuzcldc  10678  ioom  10705  elicore  10711  flqltp1  10726  flapge  10730  addmodlteq  10848  expcl2lemap  11001  expap0i  11021  hashennnuni  11232  hashf1lem2  11300  hashdmprop2dom  11310  wrdexb  11330  swrdsbslen  11452  swrdspsleq  11453  crre  11636  sq01  11674  caucvgre  11761  cvg1nlemcau  11764  cvg1nlemres  11765  resqrexlemoverl  11801  sqrtge0  11813  fimaxre2  12008  climi  12069  reccn2ap  12095  climge0  12107  nnf1o  12159  sumpr  12196  fsump1i  12216  fsum00  12245  fsumparts  12253  mertenslemi1  12318  addsin  12525  subsin  12526  addcos  12529  subcos  12530  sinbnd2  12537  cosbnd2  12538  sinltxirr  12544  dvdsaddre2b  12624  evenelz  12650  4dvdseven  12700  gcd0id  12772  gcd1  12780  bezoutlemstep  12790  dvdsgcdb  12806  mulgcd  12809  gcdzeq  12815  dvdsmulgcd  12818  sqgcd  12822  dvdssqlem  12823  bezoutr  12825  uzwodc  12830  nninfctlemfo  12833  lcmval  12857  lcmcllem  12861  lcmgcdlem  12871  lcmdvds  12873  lcmgcdeq  12877  lcmdvdsb  12878  mulgcddvds  12888  rpmulgcd2  12889  qredeu  12891  rpdvds  12893  divgcdcoprm0  12895  isprm3  12912  divgcdodd  12938  coprm  12939  rpexp  12948  sqrt2irr  12957  qdencl  12985  qeqnumdivden  12990  divnumden  12992  divdenle  12993  densq  13000  phimullem  13023  eulerthlem1  13025  eulerthlemrprm  13027  eulerthlemth  13030  prmdiveq  13034  prmdivdiv  13035  hashgcdeq  13038  phisum  13039  odzid  13043  reumodprminv  13052  oddn2prm  13060  pythagtriplem4  13067  pythagtriplem11  13073  pythagtriplem13  13075  pythagtriplem19  13081  pclemub  13086  pcprendvds2  13090  pcpre1  13091  pcpremul  13092  pceulem  13093  pczdvds  13113  pc2dvds  13129  pcaddlem  13138  pcmpt  13142  pcmpt2  13143  pcmptdvds  13144  pcprod  13145  pockthlem  13155  pockthg  13156  prmunb  13161  1arithlem4  13165  4sqlem7  13183  4sqlem8  13184  4sqlem9  13185  4sqlem10  13186  4sqlemffi  13195  4sqlem15  13204  4sqlem16  13205  4sqlem17  13206  4sqlem18  13207  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemsf1o  13306  ballotfilemscr  13311  ballotfilemrv  13312  ballotfilemfrci  13320  ballotfilemfrceq  13321  ballotfilemrinv0  13325  ennnfonelemom  13348  ennnfonelemex  13354  ennnfonelemf1  13358  ctiunctlemu1st  13374  ctiunctlemu2nd  13375  fnpr2ob  13710  mgmlrid  13748  gzsumfzval  13760  gzsumval2  13763  mndrid  13798  grpinvcnv  13922  dfgrp3mlem  13952  eqglact  14077  ghmgrp2  14098  ghmlin  14100  ghmnsgpreima  14121  kerf1ghm  14126  gzsumsplit0  14197  prdsmndd  14243  prdsgrpd  14246  prdsinvgd  14247  srgdilem  14322  srgdir  14328  srgridm  14333  ringdilem  14365  ringdir  14373  ringridm  14378  unitmulcl  14469  unitnegcl  14486  rhmmhm  14515  elrhmunit  14533  lringuplu  14552  subrgring  14581  subrg1cl  14586  qusrhm  14914  znunit  15043  znrrg  15044  assaassr  15054  assaring  15056  psrbagfsupp  15104  psrbaglecl  15109  psrbagcon  15111  psrbagconcl  15112  psrelbas  15115  mplsubgfilemcl  15139  mplsubgfileminv  15140  inopn  15153  restbasg  15318  ssrest  15332  cntop2  15352  icnpimaex  15361  cnima  15370  lmfss  15394  lmtopcnp  15400  txhmeo  15469  txswaphmeo  15471  psmet0  15477  psmettri2  15478  blhalf  15558  bdxmet  15651  xmetxpbl  15658  ioo2bl  15701  tgioo  15704  cncfi  15728  rescncf  15731  cdivcncfap  15754  cnopnap  15761  divcncfap  15764  dedekindeulemeu  15772  dedekindicclemeu  15781  ivthinclemum  15785  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthinclemdisj  15790  ivthdec  15794  ivthreinc  15795  limcimo  15815  cnplimcim  15817  cnplimclemr  15819  cnlimci  15823  limccnpcntop  15825  limccnp2lem  15826  limccnp2cntop  15827  limccoap  15828  reldvg  15829  dvbsssg  15836  dvfgg  15838  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvrecap  15863  plyco  15909  plycj  15911  plyrecj  15913  sin0pilem1  15932  sin0pilem2  15933  tanrpcl  15988  tangtx  15989  cos0pilt1  16003  logbgcd1irraplemexp  16123  zprmlogbaplem2  16135  zprmlogbaplem3  16136  ppiqsval2  16157  mpodvdsmulf1o  16185  perfect  16199  bposlem3  16211  bposlem5  16213  lgsne0  16255  lgseisen  16291  lgsquad2lem2  16299  2sqlem8a  16339  2sqlem8  16340  structgrssiedg  16382  uhgrm  16417  umgredgne  16489  usgruspgrben  16525  usgredgppren  16536  umgr2edg  16546  vtxdumgrfival  16637  wlkpropg  16663  wlkv  16665  wlkvtxeledgg  16683  g0wlk0  16709  trlsv  16723  clwwlknlen  16750  eupthv  16785  eupthf1o  16789  eupth2lem3lem4fi  16812  eulerpathprum  16819  bj-charfunbi  16935  bj-inf2vnlem1  17094  pwf1oexmid  17127  subctctexmid  17128  iooref1o  17181  taupi  17221  als2d  17232  rals2d  17234  alseu2d  17268  ralseu2d  17270