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  3225  unssbd  3399  opth  4355  potr  4431  frind  4475  brrelex2  4793  funinsn  5407  feu  5551  fcnvres  5552  fun11iun  5637  funopsn  5862  elmpocl2  6253  uchoice  6333  oprssdmm  6367  fczsupp0  6461  tfrlem1  6541  tfrlemisucfn  6557  tfrlemisucaccv  6558  tfrlemibxssdm  6560  tfrlemibfn  6561  tfrlemi14d  6566  swoer  6797  elmapssres  6909  mapsspm  6918  pmsspw  6919  mapss  6928  dom0  7093  xpf1o  7099  sbthlemi8  7236  sbthlemi9  7237  fsuppimpd  7248  supelti  7295  supisoti  7303  djulclb  7348  nninfninc  7416  nnnninfeq2  7422  cardcl  7479  isnumi  7480  cardval3ex  7483  exmidonfinlem  7498  en2eleq  7500  finacn  7513  acfun  7516  exmidaclem  7517  pw1if  7537  papirr  7564  dftap2  7570  exmidapne  7579  ccfunen  7583  acnccim  7591  indpi  7662  dfplpq2  7674  ltbtwnnq  7736  enq0tr  7754  nqnq0pi  7758  elnp1st2nd  7796  prcunqu  7805  prnmaxl  7808  prloc  7811  genpcuu  7840  addnqprllem  7847  addlocprlemeq  7853  addlocprlemgt  7854  addlocpr  7856  nqprxx  7866  gtnqex  7870  appdivnq  7883  prmuloclemcalc  7885  prmuloc  7886  mullocprlem  7890  ltprordil  7909  ltnqpri  7914  ltexprlemm  7920  ltexprlemopl  7921  ltexprlemlol  7922  ltexprlemopu  7923  ltexprlemupu  7924  ltexprlemdisj  7926  ltexprlemloc  7927  ltexprlemfl  7929  ltexprlemrl  7930  ltexprlemfu  7931  ltexprlemru  7932  ltexpri  7933  recexprlemell  7942  recexprlemelu  7943  recexprlemloc  7951  recexprlempr  7952  recexprlem1ssl  7953  recexprlem1ssu  7954  recexprlemss1l  7955  aptipr  7961  cauappcvgprlemlol  7967  cauappcvgprlemupu  7969  cauappcvgprlemladdfu  7974  cauappcvgprlemladdfl  7975  cauappcvgprlemladdrl  7977  caucvgprlemnkj  7986  caucvgprlemnbj  7987  caucvgprlemlol  7990  caucvgprlemupu  7992  caucvgprlemladdfu  7997  caucvgprlem1  7999  caucvgprlem2  8000  caucvgprprlemnjltk  8011  caucvgprprlemnbj  8013  caucvgprprlemlol  8018  caucvgprprlemupu  8020  caucvgprprlemexbt  8026  caucvgprprlem1  8029  caucvgprprlem2  8030  suplocexprlemrl  8037  suplocexprlemru  8039  suplocexprlemdisj  8040  suplocexprlemub  8043  suplocexprlemlub  8044  ltsrprg  8067  gt0srpr  8068  recexgt0sr  8093  addgt0sr  8095  mulgt0sr  8098  map2psrprg  8125  suplocsrlemb  8126  suplocsrlem  8128  nnindnn  8213  axcaucvglemcau  8218  axpre-suploclemres  8221  apreap  8866  apreim  8882  mulge0  8898  apti  8901  mulap0bbd  8939  lble  9226  nnind  9258  recnz  9677  uzind  9695  eluzadd  9889  eluzsub  9890  ixxss1  10243  ixxss2  10244  ixxss12  10245  iccss2  10283  iccssioo2  10285  iccssico2  10286  elfzolt2  10498  infssuzcldc  10602  ioom  10627  elicore  10633  flqltp1  10646  addmodlteq  10767  expcl2lemap  10920  expap0i  10940  hashennnuni  11150  hashdmprop2dom  11224  wrdexb  11244  swrdsbslen  11366  swrdspsleq  11367  crre  11550  caucvgre  11674  cvg1nlemcau  11677  cvg1nlemres  11678  resqrexlemoverl  11714  sqrtge0  11726  fimaxre2  11920  climi  11980  reccn2ap  12006  climge0  12018  nnf1o  12070  sumpr  12107  fsump1i  12127  fsum00  12156  fsumparts  12164  mertenslemi1  12229  addsin  12436  subsin  12437  addcos  12440  subcos  12441  sinbnd2  12448  cosbnd2  12449  sinltxirr  12455  dvdsaddre2b  12535  evenelz  12561  4dvdseven  12611  gcd0id  12683  gcd1  12691  bezoutlemstep  12701  dvdsgcdb  12717  mulgcd  12720  gcdzeq  12726  dvdsmulgcd  12729  sqgcd  12733  dvdssqlem  12734  bezoutr  12736  uzwodc  12741  nninfctlemfo  12744  lcmval  12768  lcmcllem  12772  lcmgcdlem  12782  lcmdvds  12784  lcmgcdeq  12788  lcmdvdsb  12789  mulgcddvds  12799  rpmulgcd2  12800  qredeu  12802  rpdvds  12804  divgcdcoprm0  12806  isprm3  12823  divgcdodd  12848  coprm  12849  rpexp  12858  sqrt2irr  12867  qdencl  12894  qeqnumdivden  12899  divnumden  12901  divdenle  12902  densq  12909  phimullem  12930  eulerthlem1  12932  eulerthlemrprm  12934  eulerthlemth  12937  prmdiveq  12941  prmdivdiv  12942  hashgcdeq  12945  phisum  12946  odzid  12950  reumodprminv  12959  oddn2prm  12967  pythagtriplem4  12974  pythagtriplem11  12980  pythagtriplem13  12982  pythagtriplem19  12988  pclemub  12993  pcprendvds2  12997  pcpre1  12998  pcpremul  12999  pceulem  13000  pczdvds  13020  pc2dvds  13036  pcaddlem  13045  pcmpt  13049  pcmpt2  13050  pcmptdvds  13051  pcprod  13052  pockthlem  13062  pockthg  13063  prmunb  13068  1arithlem4  13072  4sqlem7  13090  4sqlem8  13091  4sqlem9  13092  4sqlem10  13093  4sqlemffi  13102  4sqlem15  13111  4sqlem16  13112  4sqlem17  13113  4sqlem18  13114  ballotfilem2  13153  ballotfilemfc0  13157  ballotfilemfcc  13158  ennnfonelemom  13180  ennnfonelemex  13186  ennnfonelemf1  13190  ctiunctlemu1st  13206  ctiunctlemu2nd  13207  fnpr2ob  13574  mgmlrid  13613  gsumfzval  13625  gsumval2  13631  mndrid  13670  prdsmndd  13682  grpinvcnv  13802  dfgrp3mlem  13832  prdsgrpd  13843  prdsinvgd  13844  eqglact  13963  ghmgrp2  13984  ghmlin  13986  ghmnsgpreima  14007  kerf1ghm  14012  gsumsplit0  14084  srgdilem  14134  srgdir  14140  srgridm  14145  ringdilem  14177  ringdir  14184  ringridm  14189  unitmulcl  14280  unitnegcl  14297  rhmmhm  14326  elrhmunit  14344  lringuplu  14363  subrgring  14392  subrg1cl  14397  qusrhm  14725  znunit  14856  znrrg  14857  psrbagfsupp  14868  psrbaglecl  14873  psrbagcon  14875  psrbagconcl  14876  psrelbas  14879  mplsubgfilemcl  14903  mplsubgfileminv  14904  inopn  14917  restbasg  15082  ssrest  15096  cntop2  15116  icnpimaex  15125  cnima  15134  lmfss  15158  lmtopcnp  15164  txhmeo  15233  txswaphmeo  15235  psmet0  15241  psmettri2  15242  blhalf  15322  bdxmet  15415  xmetxpbl  15422  ioo2bl  15465  tgioo  15468  cncfi  15492  rescncf  15495  cdivcncfap  15518  cnopnap  15525  divcncfap  15528  dedekindeulemeu  15536  dedekindicclemeu  15545  ivthinclemum  15549  ivthinclemlopn  15550  ivthinclemuopn  15552  ivthinclemdisj  15554  ivthdec  15558  ivthreinc  15559  limcimo  15579  cnplimcim  15581  cnplimclemr  15583  cnlimci  15587  limccnpcntop  15589  limccnp2lem  15590  limccnp2cntop  15591  limccoap  15592  reldvg  15593  dvbsssg  15600  dvfgg  15602  dvaddxxbr  15615  dvmulxxbr  15616  dvcoapbr  15621  dvcjbr  15622  dvrecap  15627  plyco  15673  plycj  15675  plyrecj  15677  sin0pilem1  15695  sin0pilem2  15696  tanrpcl  15751  tangtx  15752  cos0pilt1  15766  logbgcd1irraplemexp  15882  mpodvdsmulf1o  15907  perfect  15918  lgsne0  15960  lgseisen  15996  lgsquad2lem2  16004  2sqlem8a  16044  2sqlem8  16045  structgrssiedg  16087  uhgrm  16122  umgredgne  16194  usgruspgrben  16230  usgredgppren  16241  umgr2edg  16251  vtxdumgrfival  16342  wlkpropg  16368  wlkv  16370  wlkvtxeledgg  16388  g0wlk0  16414  trlsv  16428  clwwlknlen  16455  eupthv  16490  eupthf1o  16494  eupth2lem3lem4fi  16517  eulerpathprum  16524  bj-charfunbi  16630  bj-inf2vnlem1  16789  pwf1oexmid  16822  subctctexmid  16823  iooref1o  16867  taupi  16908  alsi2d  16928  alsc2d  16930