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  530  simprld  532  simprrd  534  simp2  1025  simp3  1026  sbh  1825  eldifbd  3226  unssbd  3401  opth  4358  potr  4434  frind  4478  brrelex2  4796  funinsn  5410  feu  5554  fcnvres  5555  fun11iun  5640  funopsn  5865  elmpocl2  6259  uchoice  6344  oprssdmm  6378  fczsupp0  6472  tfrlem1  6552  tfrlemisucfn  6568  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemi14d  6577  swoer  6808  elmapssres  6920  mapsspm  6929  pmsspw  6930  mapss  6939  dom0  7104  xpf1o  7110  sbthlemi8  7247  sbthlemi9  7248  fsuppimpd  7259  supelti  7306  supisoti  7314  djulclb  7359  nninfninc  7427  nnnninfeq2  7433  cardcl  7490  isnumi  7491  cardval3ex  7494  exmidonfinlem  7509  en2eleq  7511  finacn  7524  acfun  7527  exmidaclem  7528  pw1if  7548  papirr  7575  dftap2  7581  exmidapne  7590  ccfunen  7594  acnccim  7602  indpi  7673  dfplpq2  7685  ltbtwnnq  7747  enq0tr  7765  nqnq0pi  7769  elnp1st2nd  7807  prcunqu  7816  prnmaxl  7819  prloc  7822  genpcuu  7851  addnqprllem  7858  addlocprlemeq  7864  addlocprlemgt  7865  addlocpr  7867  nqprxx  7877  gtnqex  7881  appdivnq  7894  prmuloclemcalc  7896  prmuloc  7897  mullocprlem  7901  ltprordil  7920  ltnqpri  7925  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  ltexpri  7944  recexprlemell  7953  recexprlemelu  7954  recexprlemloc  7962  recexprlempr  7963  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  aptipr  7972  cauappcvgprlemlol  7978  cauappcvgprlemupu  7980  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdrl  7988  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemlol  8001  caucvgprlemupu  8003  caucvgprlemladdfu  8008  caucvgprlem1  8010  caucvgprlem2  8011  caucvgprprlemnjltk  8022  caucvgprprlemnbj  8024  caucvgprprlemlol  8029  caucvgprprlemupu  8031  caucvgprprlemexbt  8037  caucvgprprlem1  8040  caucvgprprlem2  8041  suplocexprlemrl  8048  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemub  8054  suplocexprlemlub  8055  ltsrprg  8078  gt0srpr  8079  recexgt0sr  8104  addgt0sr  8106  mulgt0sr  8109  map2psrprg  8136  suplocsrlemb  8137  suplocsrlem  8139  nnindnn  8224  axcaucvglemcau  8229  axpre-suploclemres  8232  apreap  8879  apreim  8895  mulge0  8911  apti  8914  mulap0bbd  8952  lble  9241  nnind  9273  recnz  9692  uzind  9710  eluzadd  9904  eluzsub  9905  ixxss1  10259  ixxss2  10260  ixxss12  10261  iccss2  10299  iccssioo2  10301  iccssico2  10302  elfzolt2  10516  infssuzcldc  10620  ioom  10647  elicore  10653  flqltp1  10666  addmodlteq  10787  expcl2lemap  10940  expap0i  10960  hashennnuni  11170  hashdmprop2dom  11244  wrdexb  11264  swrdsbslen  11386  swrdspsleq  11387  crre  11570  caucvgre  11694  cvg1nlemcau  11697  cvg1nlemres  11698  resqrexlemoverl  11734  sqrtge0  11746  fimaxre2  11940  climi  12000  reccn2ap  12026  climge0  12038  nnf1o  12090  sumpr  12127  fsump1i  12147  fsum00  12176  fsumparts  12184  mertenslemi1  12249  addsin  12456  subsin  12457  addcos  12460  subcos  12461  sinbnd2  12468  cosbnd2  12469  sinltxirr  12475  dvdsaddre2b  12555  evenelz  12581  4dvdseven  12631  gcd0id  12703  gcd1  12711  bezoutlemstep  12721  dvdsgcdb  12737  mulgcd  12740  gcdzeq  12746  dvdsmulgcd  12749  sqgcd  12753  dvdssqlem  12754  bezoutr  12756  uzwodc  12761  nninfctlemfo  12764  lcmval  12788  lcmcllem  12792  lcmgcdlem  12802  lcmdvds  12804  lcmgcdeq  12808  lcmdvdsb  12809  mulgcddvds  12819  rpmulgcd2  12820  qredeu  12822  rpdvds  12824  divgcdcoprm0  12826  isprm3  12843  divgcdodd  12868  coprm  12869  rpexp  12878  sqrt2irr  12887  qdencl  12914  qeqnumdivden  12919  divnumden  12921  divdenle  12922  densq  12929  phimullem  12950  eulerthlem1  12952  eulerthlemrprm  12954  eulerthlemth  12957  prmdiveq  12961  prmdivdiv  12962  hashgcdeq  12965  phisum  12966  odzid  12970  reumodprminv  12979  oddn2prm  12987  pythagtriplem4  12994  pythagtriplem11  13000  pythagtriplem13  13002  pythagtriplem19  13008  pclemub  13013  pcprendvds2  13017  pcpre1  13018  pcpremul  13019  pceulem  13020  pczdvds  13040  pc2dvds  13056  pcaddlem  13065  pcmpt  13069  pcmpt2  13070  pcmptdvds  13071  pcprod  13072  pockthlem  13082  pockthg  13083  prmunb  13088  1arithlem4  13092  4sqlem7  13110  4sqlem8  13111  4sqlem9  13112  4sqlem10  13113  4sqlemffi  13122  4sqlem15  13131  4sqlem16  13132  4sqlem17  13133  4sqlem18  13134  ballotfilem2  13175  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemi1  13192  ballotfilemii  13193  ballotfilemic  13197  ballotfilem1c  13198  ballotfilemsf1o  13204  ballotfilemscr  13209  ballotfilemrv  13210  ballotfilemfrci  13218  ballotfilemfrceq  13219  ballotfilemrinv0  13223  ennnfonelemom  13246  ennnfonelemex  13252  ennnfonelemf1  13256  ctiunctlemu1st  13272  ctiunctlemu2nd  13273  fnpr2ob  13607  mgmlrid  13645  gsumfzval  13657  gsumval2  13663  mndrid  13700  grpinvcnv  13826  dfgrp3mlem  13856  eqglact  13981  ghmgrp2  14002  ghmlin  14004  ghmnsgpreima  14025  kerf1ghm  14030  gsumsplit0  14102  prdsmndd  14139  prdsgrpd  14142  prdsinvgd  14143  srgdilem  14215  srgdir  14221  srgridm  14226  ringdilem  14258  ringdir  14265  ringridm  14270  unitmulcl  14361  unitnegcl  14378  rhmmhm  14407  elrhmunit  14425  lringuplu  14444  subrgring  14473  subrg1cl  14478  qusrhm  14805  znunit  14936  znrrg  14937  psrbagfsupp  14948  psrbaglecl  14953  psrbagcon  14955  psrbagconcl  14956  psrelbas  14959  mplsubgfilemcl  14983  mplsubgfileminv  14984  inopn  14997  restbasg  15162  ssrest  15176  cntop2  15196  icnpimaex  15205  cnima  15214  lmfss  15238  lmtopcnp  15244  txhmeo  15313  txswaphmeo  15315  psmet0  15321  psmettri2  15322  blhalf  15402  bdxmet  15495  xmetxpbl  15502  ioo2bl  15545  tgioo  15548  cncfi  15572  rescncf  15575  cdivcncfap  15598  cnopnap  15605  divcncfap  15608  dedekindeulemeu  15616  dedekindicclemeu  15625  ivthinclemum  15629  ivthinclemlopn  15630  ivthinclemuopn  15632  ivthinclemdisj  15634  ivthdec  15638  ivthreinc  15639  limcimo  15659  cnplimcim  15661  cnplimclemr  15663  cnlimci  15667  limccnpcntop  15669  limccnp2lem  15670  limccnp2cntop  15671  limccoap  15672  reldvg  15673  dvbsssg  15680  dvfgg  15682  dvaddxxbr  15695  dvmulxxbr  15696  dvcoapbr  15701  dvcjbr  15702  dvrecap  15707  plyco  15753  plycj  15755  plyrecj  15757  sin0pilem1  15775  sin0pilem2  15776  tanrpcl  15831  tangtx  15832  cos0pilt1  15846  logbgcd1irraplemexp  15962  mpodvdsmulf1o  15987  perfect  15998  lgsne0  16040  lgseisen  16076  lgsquad2lem2  16084  2sqlem8a  16124  2sqlem8  16125  structgrssiedg  16167  uhgrm  16202  umgredgne  16274  usgruspgrben  16310  usgredgppren  16321  umgr2edg  16331  vtxdumgrfival  16422  wlkpropg  16448  wlkv  16450  wlkvtxeledgg  16468  g0wlk0  16494  trlsv  16508  clwwlknlen  16535  eupthv  16570  eupthf1o  16574  eupth2lem3lem4fi  16597  eulerpathprum  16604  bj-charfunbi  16720  bj-inf2vnlem1  16879  pwf1oexmid  16912  subctctexmid  16913  iooref1o  16957  taupi  16998  alsi2d  17007  alsc2d  17009