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  4379  potr  4455  frind  4499  brrelex2  4818  funinsn  5433  feu  5577  fcnvres  5578  fun11iun  5663  funopsn  5894  elmpocl2  6289  uchoice  6375  oprssdmm  6409  fczsupp0  6503  tfrlem1  6583  tfrlemisucfn  6599  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemi14d  6608  swoer  6839  elmapssres  6958  mapsspm  6967  pmsspw  6968  mapss  6977  dom0  7142  xpf1o  7148  sbthlemi8  7286  sbthlemi9  7287  fsuppimpd  7298  supelti  7348  supisoti  7356  djulclb  7401  nninfninc  7469  nnnninfeq2  7475  cardcl  7532  isnumi  7533  cardval3ex  7536  exmidonfinlem  7551  en2eleq  7553  finacn  7566  acfun  7569  exmidaclem  7570  pw1if  7590  papirr  7617  dftap2  7623  exmidapne  7632  ccfunen  7636  acnccim  7644  indpi  7715  dfplpq2  7727  ltbtwnnq  7789  enq0tr  7807  nqnq0pi  7811  elnp1st2nd  7849  prcunqu  7858  prnmaxl  7861  prloc  7864  genpcuu  7893  addnqprllem  7900  addlocprlemeq  7906  addlocprlemgt  7907  addlocpr  7909  nqprxx  7919  gtnqex  7923  appdivnq  7936  prmuloclemcalc  7938  prmuloc  7939  mullocprlem  7943  ltprordil  7962  ltnqpri  7967  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  ltexpri  7986  recexprlemell  7995  recexprlemelu  7996  recexprlemloc  8004  recexprlempr  8005  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  aptipr  8014  cauappcvgprlemlol  8020  cauappcvgprlemupu  8022  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdrl  8030  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemlol  8043  caucvgprlemupu  8045  caucvgprlemladdfu  8050  caucvgprlem1  8052  caucvgprlem2  8053  caucvgprprlemnjltk  8064  caucvgprprlemnbj  8066  caucvgprprlemlol  8071  caucvgprprlemupu  8073  caucvgprprlemexbt  8079  caucvgprprlem1  8082  caucvgprprlem2  8083  suplocexprlemrl  8090  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemub  8096  suplocexprlemlub  8097  ltsrprg  8120  gt0srpr  8121  recexgt0sr  8146  addgt0sr  8148  mulgt0sr  8151  map2psrprg  8178  suplocsrlemb  8179  suplocsrlem  8181  nnindnn  8266  axcaucvglemcau  8271  axpre-suploclemres  8274  apreap  8923  apreim  8939  mulge0  8955  apti  8958  mulap0bbd  8996  lble  9285  nnind  9329  recnz  9750  uzind  9768  eluzadd  9967  eluzsub  9968  ixxss1  10323  ixxss2  10324  ixxss12  10325  iccss2  10363  iccssioo2  10365  iccssico2  10366  elfzolt2  10581  infssuzcldc  10685  ioom  10712  elicore  10718  flqltp1  10733  flapge  10737  flaplt  10739  addmodlteq  10856  expcl2lemap  11009  expap0i  11029  hashennnuni  11240  hashf1lem2  11308  hashdmprop2dom  11318  wrdexb  11338  swrdsbslen  11460  swrdspsleq  11461  crre  11644  sq01  11682  caucvgre  11769  cvg1nlemcau  11772  cvg1nlemres  11773  resqrexlemoverl  11809  sqrtge0  11821  fimaxre2  12016  climi  12078  reccn2ap  12104  climge0  12116  nnf1o  12168  sumpr  12205  fsump1i  12225  fsum00  12254  fsumparts  12262  mertenslemi1  12327  addsin  12534  subsin  12535  addcos  12538  subcos  12539  sinbnd2  12546  cosbnd2  12547  sinltxirr  12553  dvdsaddre2b  12633  evenelz  12659  4dvdseven  12709  gcd0id  12781  gcd1  12789  bezoutlemstep  12799  dvdsgcdb  12815  mulgcd  12818  gcdzeq  12824  dvdsmulgcd  12827  sqgcd  12831  dvdssqlem  12832  bezoutr  12834  uzwodc  12839  nninfctlemfo  12842  lcmval  12866  lcmcllem  12870  lcmgcdlem  12880  lcmdvds  12882  lcmgcdeq  12886  lcmdvdsb  12887  mulgcddvds  12897  rpmulgcd2  12898  qredeu  12900  rpdvds  12902  divgcdcoprm0  12904  isprm3  12921  divgcdodd  12947  coprm  12948  rpexp  12957  sqrt2irr  12966  qdencl  12994  qeqnumdivden  12999  divnumden  13001  divdenle  13002  densq  13009  phimullem  13032  eulerthlem1  13034  eulerthlemrprm  13036  eulerthlemth  13039  prmdiveq  13043  prmdivdiv  13044  hashgcdeq  13047  phisum  13048  odzid  13052  reumodprminv  13061  oddn2prm  13069  pythagtriplem4  13076  pythagtriplem11  13082  pythagtriplem13  13084  pythagtriplem19  13090  pclemub  13095  pcprendvds2  13099  pcpre1  13100  pcpremul  13101  pceulem  13102  pczdvds  13122  pc2dvds  13138  pcaddlem  13147  pcmpt  13151  pcmpt2  13152  pcmptdvds  13153  pcprod  13154  pockthlem  13164  pockthg  13165  prmunb  13170  1arithlem4  13174  4sqlem7  13192  4sqlem8  13193  4sqlem9  13194  4sqlem10  13195  4sqlemffi  13204  4sqlem15  13213  4sqlem16  13214  4sqlem17  13215  4sqlem18  13216  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemsf1o  13315  ballotfilemscr  13320  ballotfilemrv  13321  ballotfilemfrci  13329  ballotfilemfrceq  13330  ballotfilemrinv0  13334  ennnfonelemom  13357  ennnfonelemex  13363  ennnfonelemf1  13367  ctiunctlemu1st  13383  ctiunctlemu2nd  13384  fnpr2ob  13720  mgmlrid  13758  gzsumfzval  13770  gzsumval2  13773  mndrid  13808  grpinvcnv  13932  dfgrp3mlem  13962  eqglact  14087  ghmgrp2  14108  ghmlin  14110  ghmnsgpreima  14131  kerf1ghm  14136  resscntz  14166  cntzmhm  14173  gzsumsplit0  14238  prdsmndd  14301  prdsgrpd  14304  prdsinvgd  14305  srgdilem  14380  srgdir  14386  srgridm  14391  ringdilem  14423  ringdir  14431  ringridm  14436  unitmulcl  14529  unitnegcl  14546  rhmmhm  14575  elrhmunit  14593  lringuplu  14612  subrgring  14641  subrg1cl  14646  qusrhm  14974  znunit  15103  znrrg  15104  assaassr  15114  assaring  15116  psrbagfsupp  15164  psrbaglecl  15169  psrbagcon  15171  psrbagconcl  15173  gsumbagdiaglem  15175  psrelbas  15179  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  mplsubgfilemcl  15215  mplsubgfileminv  15216  inopn  15229  restbasg  15394  ssrest  15408  cntop2  15428  icnpimaex  15437  cnima  15446  lmfss  15470  lmtopcnp  15476  txhmeo  15545  txswaphmeo  15547  psmet0  15553  psmettri2  15554  blhalf  15634  bdxmet  15727  xmetxpbl  15734  ioo2bl  15777  tgioo  15780  cncfi  15804  rescncf  15807  cdivcncfap  15830  cnopnap  15837  divcncfap  15840  dedekindeulemeu  15848  dedekindicclemeu  15857  ivthinclemum  15861  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthinclemdisj  15866  ivthdec  15870  ivthreinc  15871  limcimo  15891  cnplimcim  15893  cnplimclemr  15895  cnlimci  15899  limccnpcntop  15901  limccnp2lem  15902  limccnp2cntop  15903  limccoap  15904  reldvg  15905  dvbsssg  15912  dvfgg  15914  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvrecap  15939  plyco  15985  plycj  15987  plyrecj  15989  sin0pilem1  16008  sin0pilem2  16009  tanrpcl  16064  tangtx  16065  cos0pilt1  16080  logbgcd1irraplemexp  16204  zprmlogbaplem2  16216  zprmlogbaplem3  16217  ppiqsval2  16241  chtqge0  16247  chtqwordi  16263  mpodvdsmulf1o  16284  perfect  16301  bposlem3  16313  bposlem5  16315  bposlem6  16316  bposlem9  16319  lgsne0  16362  lgseisen  16398  lgsquad2lem2  16406  2sqlem8a  16446  2sqlem8  16447  structgrssiedg  16489  uhgrm  16524  umgredgne  16596  usgruspgrben  16632  usgredgppren  16643  umgr2edg  16653  vtxdumgrfival  16744  wlkpropg  16770  wlkv  16772  wlkvtxeledgg  16790  g0wlk0  16816  trlsv  16830  clwwlknlen  16857  eupthv  16892  eupthf1o  16896  eupth2lem3lem4fi  16919  eulerpathprum  16926  bj-charfunbi  17042  bj-inf2vnlem1  17201  pwf1oexmid  17234  subctctexmid  17235  idjudju  17252  iooref1o  17289  taupi  17330  als2d  17341  rals2d  17343  alseu2d  17377  ralseu2d  17379