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	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simprd	⊢ (𝜑 → 𝜒)

Proof of Theorem simprd

Step	Hyp	Ref	Expression
1		simprd.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
2		simpr 110	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜒)

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  4375  potr  4451  frind  4495  brrelex2  4814  funinsn  5428  feu  5572  fcnvres  5573  fun11iun  5658  funopsn  5885  elmpocl2  6280  uchoice  6365  oprssdmm  6399  fczsupp0  6493  tfrlem1  6573  tfrlemisucfn  6589  tfrlemisucaccv  6590  tfrlemibxssdm  6592  tfrlemibfn  6593  tfrlemi14d  6598  swoer  6829  elmapssres  6948  mapsspm  6957  pmsspw  6958  mapss  6967  dom0  7132  xpf1o  7138  sbthlemi8  7275  sbthlemi9  7276  fsuppimpd  7287  supelti  7336  supisoti  7344  djulclb  7389  nninfninc  7457  nnnninfeq2  7463  cardcl  7520  isnumi  7521  cardval3ex  7524  exmidonfinlem  7539  en2eleq  7541  finacn  7554  acfun  7557  exmidaclem  7558  pw1if  7578  papirr  7605  dftap2  7611  exmidapne  7620  ccfunen  7624  acnccim  7632  indpi  7703  dfplpq2  7715  ltbtwnnq  7777  enq0tr  7795  nqnq0pi  7799  elnp1st2nd  7837  prcunqu  7846  prnmaxl  7849  prloc  7852  genpcuu  7881  addnqprllem  7888  addlocprlemeq  7894  addlocprlemgt  7895  addlocpr  7897  nqprxx  7907  gtnqex  7911  appdivnq  7924  prmuloclemcalc  7926  prmuloc  7927  mullocprlem  7931  ltprordil  7950  ltnqpri  7955  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemlol  7963  ltexprlemopu  7964  ltexprlemupu  7965  ltexprlemdisj  7967  ltexprlemloc  7968  ltexprlemfl  7970  ltexprlemrl  7971  ltexprlemfu  7972  ltexprlemru  7973  ltexpri  7974  recexprlemell  7983  recexprlemelu  7984  recexprlemloc  7992  recexprlempr  7993  recexprlem1ssl  7994  recexprlem1ssu  7995  recexprlemss1l  7996  aptipr  8002  cauappcvgprlemlol  8008  cauappcvgprlemupu  8010  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  cauappcvgprlemladdrl  8018  caucvgprlemnkj  8027  caucvgprlemnbj  8028  caucvgprlemlol  8031  caucvgprlemupu  8033  caucvgprlemladdfu  8038  caucvgprlem1  8040  caucvgprlem2  8041  caucvgprprlemnjltk  8052  caucvgprprlemnbj  8054  caucvgprprlemlol  8059  caucvgprprlemupu  8061  caucvgprprlemexbt  8067  caucvgprprlem1  8070  caucvgprprlem2  8071  suplocexprlemrl  8078  suplocexprlemru  8080  suplocexprlemdisj  8081  suplocexprlemub  8084  suplocexprlemlub  8085  ltsrprg  8108  gt0srpr  8109  recexgt0sr  8134  addgt0sr  8136  mulgt0sr  8139  map2psrprg  8166  suplocsrlemb  8167  suplocsrlem  8169  nnindnn  8254  axcaucvglemcau  8259  axpre-suploclemres  8262  apreap  8909  apreim  8925  mulge0  8941  apti  8944  mulap0bbd  8982  lble  9271  nnind  9303  recnz  9722  uzind  9740  eluzadd  9934  eluzsub  9935  ixxss1  10289  ixxss2  10290  ixxss12  10291  iccss2  10329  iccssioo2  10331  iccssico2  10332  elfzolt2  10547  infssuzcldc  10651  ioom  10678  elicore  10684  flqltp1  10697  addmodlteq  10818  expcl2lemap  10971  expap0i  10991  hashennnuni  11201  hashf1lem2  11269  hashdmprop2dom  11279  wrdexb  11299  swrdsbslen  11421  swrdspsleq  11422  crre  11605  sq01  11643  caucvgre  11730  cvg1nlemcau  11733  cvg1nlemres  11734  resqrexlemoverl  11770  sqrtge0  11782  fimaxre2  11976  climi  12036  reccn2ap  12062  climge0  12074  nnf1o  12126  sumpr  12163  fsump1i  12183  fsum00  12212  fsumparts  12220  mertenslemi1  12285  addsin  12492  subsin  12493  addcos  12496  subcos  12497  sinbnd2  12504  cosbnd2  12505  sinltxirr  12511  dvdsaddre2b  12591  evenelz  12617  4dvdseven  12667  gcd0id  12739  gcd1  12747  bezoutlemstep  12757  dvdsgcdb  12773  mulgcd  12776  gcdzeq  12782  dvdsmulgcd  12785  sqgcd  12789  dvdssqlem  12790  bezoutr  12792  uzwodc  12797  nninfctlemfo  12800  lcmval  12824  lcmcllem  12828  lcmgcdlem  12838  lcmdvds  12840  lcmgcdeq  12844  lcmdvdsb  12845  mulgcddvds  12855  rpmulgcd2  12856  qredeu  12858  rpdvds  12860  divgcdcoprm0  12862  isprm3  12879  divgcdodd  12904  coprm  12905  rpexp  12914  sqrt2irr  12923  qdencl  12950  qeqnumdivden  12955  divnumden  12957  divdenle  12958  densq  12965  phimullem  12986  eulerthlem1  12988  eulerthlemrprm  12990  eulerthlemth  12993  prmdiveq  12997  prmdivdiv  12998  hashgcdeq  13001  phisum  13002  odzid  13006  reumodprminv  13015  oddn2prm  13023  pythagtriplem4  13030  pythagtriplem11  13036  pythagtriplem13  13038  pythagtriplem19  13044  pclemub  13049  pcprendvds2  13053  pcpre1  13054  pcpremul  13055  pceulem  13056  pczdvds  13076  pc2dvds  13092  pcaddlem  13101  pcmpt  13105  pcmpt2  13106  pcmptdvds  13107  pcprod  13108  pockthlem  13118  pockthg  13119  prmunb  13124  1arithlem4  13128  4sqlem7  13146  4sqlem8  13147  4sqlem9  13148  4sqlem10  13149  4sqlemffi  13158  4sqlem15  13167  4sqlem16  13168  4sqlem17  13169  4sqlem18  13170  ballotfilem2  13211  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemi1  13228  ballotfilemii  13229  ballotfilemic  13233  ballotfilem1c  13234  ballotfilemsf1o  13240  ballotfilemscr  13245  ballotfilemrv  13246  ballotfilemfrci  13254  ballotfilemfrceq  13255  ballotfilemrinv0  13259  ennnfonelemom  13282  ennnfonelemex  13288  ennnfonelemf1  13292  ctiunctlemu1st  13308  ctiunctlemu2nd  13309  fnpr2ob  13644  mgmlrid  13682  gzsumfzval  13694  gzsumval2  13697  mndrid  13732  grpinvcnv  13856  dfgrp3mlem  13886  eqglact  14011  ghmgrp2  14032  ghmlin  14034  ghmnsgpreima  14055  kerf1ghm  14060  gzsumsplit0  14131  prdsmndd  14177  prdsgrpd  14180  prdsinvgd  14181  srgdilem  14256  srgdir  14262  srgridm  14267  ringdilem  14299  ringdir  14307  ringridm  14312  unitmulcl  14403  unitnegcl  14420  rhmmhm  14449  elrhmunit  14467  lringuplu  14486  subrgring  14515  subrg1cl  14520  qusrhm  14848  znunit  14977  znrrg  14978  assaassr  14988  assaring  14990  psrbagfsupp  15038  psrbaglecl  15043  psrbagcon  15045  psrbagconcl  15046  psrelbas  15049  mplsubgfilemcl  15073  mplsubgfileminv  15074  inopn  15087  restbasg  15252  ssrest  15266  cntop2  15286  icnpimaex  15295  cnima  15304  lmfss  15328  lmtopcnp  15334  txhmeo  15403  txswaphmeo  15405  psmet0  15411  psmettri2  15412  blhalf  15492  bdxmet  15585  xmetxpbl  15592  ioo2bl  15635  tgioo  15638  cncfi  15662  rescncf  15665  cdivcncfap  15688  cnopnap  15695  divcncfap  15698  dedekindeulemeu  15706  dedekindicclemeu  15715  ivthinclemum  15719  ivthinclemlopn  15720  ivthinclemuopn  15722  ivthinclemdisj  15724  ivthdec  15728  ivthreinc  15729  limcimo  15749  cnplimcim  15751  cnplimclemr  15753  cnlimci  15757  limccnpcntop  15759  limccnp2lem  15760  limccnp2cntop  15761  limccoap  15762  reldvg  15763  dvbsssg  15770  dvfgg  15772  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  dvcjbr  15792  dvrecap  15797  plyco  15843  plycj  15845  plyrecj  15847  sin0pilem1  15865  sin0pilem2  15866  tanrpcl  15921  tangtx  15922  cos0pilt1  15936  logbgcd1irraplemexp  16053  mpodvdsmulf1o  16087  perfect  16098  lgsne0  16140  lgseisen  16176  lgsquad2lem2  16184  2sqlem8a  16224  2sqlem8  16225  structgrssiedg  16267  uhgrm  16302  umgredgne  16374  usgruspgrben  16410  usgredgppren  16421  umgr2edg  16431  vtxdumgrfival  16522  wlkpropg  16548  wlkv  16550  wlkvtxeledgg  16568  g0wlk0  16594  trlsv  16608  clwwlknlen  16635  eupthv  16670  eupthf1o  16674  eupth2lem3lem4fi  16697  eulerpathprum  16704  bj-charfunbi  16820  bj-inf2vnlem1  16979  pwf1oexmid  17012  subctctexmid  17013  iooref1o  17057  taupi  17097  als2d  17108  rals2d  17110