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  6584  tfrlemisucfn  6600  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemibfn  6604  tfrlemi14d  6609  swoer  6840  elmapssres  6959  mapsspm  6968  pmsspw  6969  mapss  6979  dom0  7144  xpf1o  7150  sbthlemi8  7288  sbthlemi9  7289  fsuppfiss  7300  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  9749  uzind  9767  eluzadd  9966  eluzsub  9967  ixxss1  10322  ixxss2  10323  ixxss12  10324  iccss2  10362  iccssioo2  10364  iccssico2  10365  elfzolt2  10580  infssuzcldc  10684  ioom  10711  elicore  10717  flqltp1  10732  flapge  10736  flaplt  10738  addmodlteq  10855  expcl2lemap  11008  expap0i  11028  hashennnuni  11239  hashf1lem2  11307  hashdmprop2dom  11317  wrdexb  11337  swrdsbslen  11459  swrdspsleq  11460  crre  11643  sq01  11681  caucvgre  11768  cvg1nlemcau  11771  cvg1nlemres  11772  resqrexlemoverl  11808  sqrtge0  11820  fimaxre2  12015  climi  12077  reccn2ap  12103  climge0  12115  nnf1o  12167  sumpr  12204  fsump1i  12224  fsum00  12253  fsumparts  12261  mertenslemi1  12326  addsin  12533  subsin  12534  addcos  12537  subcos  12538  sinbnd2  12545  cosbnd2  12546  sinltxirr  12552  dvdsaddre2b  12632  evenelz  12658  4dvdseven  12708  gcd0id  12780  gcd1  12788  bezoutlemstep  12798  dvdsgcdb  12814  mulgcd  12817  gcdzeq  12823  dvdsmulgcd  12826  sqgcd  12830  dvdssqlem  12831  bezoutr  12833  uzwodc  12838  nninfctlemfo  12841  lcmval  12865  lcmcllem  12869  lcmgcdlem  12879  lcmdvds  12881  lcmgcdeq  12885  lcmdvdsb  12886  mulgcddvds  12896  rpmulgcd2  12897  qredeu  12899  rpdvds  12901  divgcdcoprm0  12903  isprm3  12920  divgcdodd  12946  coprm  12947  rpexp  12956  sqrt2irr  12965  qdencl  12993  qeqnumdivden  12998  divnumden  13000  divdenle  13001  densq  13008  phimullem  13031  eulerthlem1  13033  eulerthlemrprm  13035  eulerthlemth  13038  prmdiveq  13042  prmdivdiv  13043  hashgcdeq  13046  phisum  13047  odzid  13051  reumodprminv  13060  oddn2prm  13068  pythagtriplem4  13075  pythagtriplem11  13081  pythagtriplem13  13083  pythagtriplem19  13089  pclemub  13094  pcprendvds2  13098  pcpre1  13099  pcpremul  13100  pceulem  13101  pczdvds  13121  pc2dvds  13137  pcaddlem  13146  pcmpt  13150  pcmpt2  13151  pcmptdvds  13152  pcprod  13153  pockthlem  13163  pockthg  13164  prmunb  13169  1arithlem4  13173  4sqlem7  13191  4sqlem8  13192  4sqlem9  13193  4sqlem10  13194  4sqlemffi  13203  4sqlem15  13212  4sqlem16  13213  4sqlem17  13214  4sqlem18  13215  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemsf1o  13314  ballotfilemscr  13319  ballotfilemrv  13320  ballotfilemfrci  13328  ballotfilemfrceq  13329  ballotfilemrinv0  13333  ennnfonelemom  13356  ennnfonelemex  13362  ennnfonelemf1  13366  ctiunctlemu1st  13382  ctiunctlemu2nd  13383  fnpr2ob  13719  mgmlrid  13757  gzsumfzval  13769  gzsumval2  13772  mndrid  13807  grpinvcnv  13931  dfgrp3mlem  13961  eqglact  14086  ghmgrp2  14107  ghmlin  14109  ghmnsgpreima  14130  kerf1ghm  14135  resscntz  14165  cntzmhm  14172  gzsumsplit0  14237  prdsmndd  14300  prdsgrpd  14303  prdsinvgd  14304  srgdilem  14379  srgdir  14385  srgridm  14390  ringdilem  14422  ringdir  14430  ringridm  14435  unitmulcl  14528  unitnegcl  14545  rhmmhm  14574  elrhmunit  14592  lringuplu  14611  subrgring  14640  subrg1cl  14645  qusrhm  14973  znunit  15102  znrrg  15103  assaassr  15113  assaring  15115  psrbagfsuppfi  15165  psrbaglecl  15172  psrbagcon  15174  psrbagconcl  15176  gsumbagdiaglem  15184  psrelbas  15188  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  mvrclfi  15226  mplsubgfilemcl  15232  mplsubgfileminv  15233  inopn  15246  restbasg  15411  ssrest  15425  cntop2  15445  icnpimaex  15454  cnima  15463  lmfss  15487  lmtopcnp  15493  txhmeo  15562  txswaphmeo  15564  psmet0  15570  psmettri2  15571  blhalf  15651  bdxmet  15744  xmetxpbl  15751  ioo2bl  15794  tgioo  15797  cncfi  15821  rescncf  15824  cdivcncfap  15847  cnopnap  15854  divcncfap  15857  dedekindeulemeu  15865  dedekindicclemeu  15874  ivthinclemum  15878  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthinclemdisj  15883  ivthdec  15887  ivthreinc  15888  limcimo  15908  cnplimcim  15910  cnplimclemr  15912  cnlimci  15916  limccnpcntop  15918  limccnp2lem  15919  limccnp2cntop  15920  limccoap  15921  reldvg  15922  dvbsssg  15929  dvfgg  15931  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvrecap  15956  plyco  16002  plycj  16004  plyrecj  16006  sin0pilem1  16025  sin0pilem2  16026  tanrpcl  16081  tangtx  16082  cos0pilt1  16097  logbgcd1irraplemexp  16221  zprmlogbaplem2  16233  zprmlogbaplem3  16234  ppiqsval2  16258  chtqge0  16264  chtqwordi  16280  mpodvdsmulf1o  16301  perfect  16318  bposlem3  16330  bposlem5  16332  bposlem6  16333  bposlem9  16336  lgsne0  16379  lgseisen  16415  lgsquad2lem2  16423  2sqlem8a  16463  2sqlem8  16464  structgrssiedg  16506  uhgrm  16541  umgredgne  16613  usgruspgrben  16649  usgredgppren  16660  umgr2edg  16670  vtxdumgrfival  16761  wlkpropg  16787  wlkv  16789  wlkvtxeledgg  16807  g0wlk0  16833  trlsv  16847  clwwlknlen  16874  eupthv  16909  eupthf1o  16913  eupth2lem3lem4fi  16936  eulerpathprum  16943  bj-charfunbi  17059  bj-inf2vnlem1  17218  pwf1oexmid  17251  subctctexmid  17252  idjudju  17269  iooref1o  17306  taupi  17347  als2d  17358  rals2d  17360  alseu2d  17394  ralseu2d  17396