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  simprld  530  simprrd  532  simp2  1022  simp3  1023  sbh  1822  eldifbd  3210  unssbd  3383  opth  4327  potr  4403  frind  4447  brrelex2  4765  funinsn  5376  feu  5516  fcnvres  5517  fun11iun  5601  funopsn  5825  elmpocl2  6214  uchoice  6295  oprssdmm  6329  tfrlem1  6469  tfrlemisucfn  6485  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrlemi14d  6494  swoer  6725  elmapssres  6837  mapsspm  6846  pmsspw  6847  mapss  6855  dom0  7019  xpf1o  7025  sbthlemi8  7157  sbthlemi9  7158  supelti  7195  supisoti  7203  djulclb  7248  nninfninc  7316  nnnninfeq2  7322  cardcl  7379  isnumi  7380  cardval3ex  7383  exmidonfinlem  7397  en2eleq  7399  finacn  7412  acfun  7415  exmidaclem  7416  pw1if  7436  dftap2  7463  exmidapne  7472  ccfunen  7476  acnccim  7484  indpi  7555  dfplpq2  7567  ltbtwnnq  7629  enq0tr  7647  nqnq0pi  7651  elnp1st2nd  7689  prcunqu  7698  prnmaxl  7701  prloc  7704  genpcuu  7733  addnqprllem  7740  addlocprlemeq  7746  addlocprlemgt  7747  addlocpr  7749  nqprxx  7759  gtnqex  7763  appdivnq  7776  prmuloclemcalc  7778  prmuloc  7779  mullocprlem  7783  ltprordil  7802  ltnqpri  7807  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemlol  7815  ltexprlemopu  7816  ltexprlemupu  7817  ltexprlemdisj  7819  ltexprlemloc  7820  ltexprlemfl  7822  ltexprlemrl  7823  ltexprlemfu  7824  ltexprlemru  7825  ltexpri  7826  recexprlemell  7835  recexprlemelu  7836  recexprlemloc  7844  recexprlempr  7845  recexprlem1ssl  7846  recexprlem1ssu  7847  recexprlemss1l  7848  aptipr  7854  cauappcvgprlemlol  7860  cauappcvgprlemupu  7862  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  cauappcvgprlemladdrl  7870  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprlemlol  7883  caucvgprlemupu  7885  caucvgprlemladdfu  7890  caucvgprlem1  7892  caucvgprlem2  7893  caucvgprprlemnjltk  7904  caucvgprprlemnbj  7906  caucvgprprlemlol  7911  caucvgprprlemupu  7913  caucvgprprlemexbt  7919  caucvgprprlem1  7922  caucvgprprlem2  7923  suplocexprlemrl  7930  suplocexprlemru  7932  suplocexprlemdisj  7933  suplocexprlemub  7936  suplocexprlemlub  7937  ltsrprg  7960  gt0srpr  7961  recexgt0sr  7986  addgt0sr  7988  mulgt0sr  7991  map2psrprg  8018  suplocsrlemb  8019  suplocsrlem  8021  nnindnn  8106  axcaucvglemcau  8111  axpre-suploclemres  8114  apreap  8760  apreim  8776  mulge0  8792  apti  8795  mulap0bbd  8833  lble  9120  nnind  9152  recnz  9566  uzind  9584  eluzadd  9778  eluzsub  9779  ixxss1  10132  ixxss2  10133  ixxss12  10134  iccss2  10172  iccssioo2  10174  iccssico2  10175  elfzolt2  10385  infssuzcldc  10488  ioom  10513  elicore  10519  flqltp1  10532  addmodlteq  10653  expcl2lemap  10806  expap0i  10826  hashennnuni  11034  hashdmprop2dom  11101  wrdexb  11118  swrdsbslen  11240  swrdspsleq  11241  crre  11411  caucvgre  11535  cvg1nlemcau  11538  cvg1nlemres  11539  resqrexlemoverl  11575  sqrtge0  11587  fimaxre2  11781  climi  11841  reccn2ap  11867  climge0  11879  nnf1o  11930  sumpr  11967  fsump1i  11987  fsum00  12016  fsumparts  12024  mertenslemi1  12089  addsin  12296  subsin  12297  addcos  12300  subcos  12301  sinbnd2  12308  cosbnd2  12309  sinltxirr  12315  dvdsaddre2b  12395  evenelz  12421  4dvdseven  12471  gcd0id  12543  gcd1  12551  bezoutlemstep  12561  dvdsgcdb  12577  mulgcd  12580  gcdzeq  12586  dvdsmulgcd  12589  sqgcd  12593  dvdssqlem  12594  bezoutr  12596  uzwodc  12601  nninfctlemfo  12604  lcmval  12628  lcmcllem  12632  lcmgcdlem  12642  lcmdvds  12644  lcmgcdeq  12648  lcmdvdsb  12649  mulgcddvds  12659  rpmulgcd2  12660  qredeu  12662  rpdvds  12664  divgcdcoprm0  12666  isprm3  12683  divgcdodd  12708  coprm  12709  rpexp  12718  sqrt2irr  12727  qdencl  12754  qeqnumdivden  12759  divnumden  12761  divdenle  12762  densq  12769  phimullem  12790  eulerthlem1  12792  eulerthlemrprm  12794  eulerthlemth  12797  prmdiveq  12801  prmdivdiv  12802  hashgcdeq  12805  phisum  12806  odzid  12810  reumodprminv  12819  oddn2prm  12827  pythagtriplem4  12834  pythagtriplem11  12840  pythagtriplem13  12842  pythagtriplem19  12848  pclemub  12853  pcprendvds2  12857  pcpre1  12858  pcpremul  12859  pceulem  12860  pczdvds  12880  pc2dvds  12896  pcaddlem  12905  pcmpt  12909  pcmpt2  12910  pcmptdvds  12911  pcprod  12912  pockthlem  12922  pockthg  12923  prmunb  12928  1arithlem4  12932  4sqlem7  12950  4sqlem8  12951  4sqlem9  12952  4sqlem10  12953  4sqlemffi  12962  4sqlem15  12971  4sqlem16  12972  4sqlem17  12973  4sqlem18  12974  ennnfonelemom  13022  ennnfonelemex  13028  ennnfonelemf1  13032  ctiunctlemu1st  13048  ctiunctlemu2nd  13049  fnpr2ob  13416  mgmlrid  13455  gsumfzval  13467  gsumval2  13473  mndrid  13512  prdsmndd  13524  grpinvcnv  13644  dfgrp3mlem  13674  prdsgrpd  13685  prdsinvgd  13686  eqglact  13805  ghmgrp2  13826  ghmlin  13828  ghmnsgpreima  13849  kerf1ghm  13854  srgdilem  13975  srgdir  13981  srgridm  13986  ringdilem  14018  ringdir  14025  ringridm  14030  unitmulcl  14120  unitnegcl  14137  rhmmhm  14166  elrhmunit  14184  lringuplu  14203  subrgring  14231  subrg1cl  14236  qusrhm  14535  znunit  14666  znrrg  14667  psrelbas  14682  mplsubgfilemcl  14706  mplsubgfileminv  14707  inopn  14720  restbasg  14885  ssrest  14899  cntop2  14919  icnpimaex  14928  cnima  14937  lmfss  14961  lmtopcnp  14967  txhmeo  15036  txswaphmeo  15038  psmet0  15044  psmettri2  15045  blhalf  15125  bdxmet  15218  xmetxpbl  15225  ioo2bl  15268  tgioo  15271  cncfi  15295  rescncf  15298  cdivcncfap  15321  cnopnap  15328  divcncfap  15331  dedekindeulemeu  15339  dedekindicclemeu  15348  ivthinclemum  15352  ivthinclemlopn  15353  ivthinclemuopn  15355  ivthinclemdisj  15357  ivthdec  15361  ivthreinc  15362  limcimo  15382  cnplimcim  15384  cnplimclemr  15386  cnlimci  15390  limccnpcntop  15392  limccnp2lem  15393  limccnp2cntop  15394  limccoap  15395  reldvg  15396  dvbsssg  15403  dvfgg  15405  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  dvcjbr  15425  dvrecap  15430  plyco  15476  plycj  15478  plyrecj  15480  sin0pilem1  15498  sin0pilem2  15499  tanrpcl  15554  tangtx  15555  cos0pilt1  15569  logbgcd1irraplemexp  15685  mpodvdsmulf1o  15707  perfect  15718  lgsne0  15760  lgseisen  15796  lgsquad2lem2  15804  2sqlem8a  15844  2sqlem8  15845  structgrssiedg  15887  uhgrm  15922  umgredgne  15994  usgruspgrben  16030  usgredgppren  16041  umgr2edg  16051  vtxdumgrfival  16109  wlkpropg  16135  wlkv  16137  wlkvtxeledgg  16155  g0wlk0  16181  trlsv  16193  clwwlknlen  16220  eupthv  16255  eupthf1o  16259  bj-charfunbi  16356  bj-inf2vnlem1  16515  pwf1oexmid  16550  subctctexmid  16551  iooref1o  16588  taupi  16627  alsi2d  16643  alsc2d  16645