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

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  6583  tfrlemisucfn  6599  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemi14d  6608  swoer  6839  elmapssres  6958  mapsspm  6967  pmsspw  6968  mapss  6978  dom0  7143  xpf1o  7149  sbthlemi8  7287  sbthlemi9  7288  fsuppimpd  7299  supelti  7349  supisoti  7357  djulclb  7402  nninfninc  7470  nnnninfeq2  7476  cardcl  7533  isnumi  7534  cardval3ex  7537  exmidonfinlem  7552  en2eleq  7554  finacn  7567  acfun  7570  exmidaclem  7571  pw1if  7591  papirr  7618  dftap2  7624  exmidapne  7633  ccfunen  7637  acnccim  7645  indpi  7716  dfplpq2  7728  ltbtwnnq  7790  enq0tr  7808  nqnq0pi  7812  elnp1st2nd  7850  prcunqu  7859  prnmaxl  7862  prloc  7865  genpcuu  7894  addnqprllem  7901  addlocprlemeq  7907  addlocprlemgt  7908  addlocpr  7910  nqprxx  7920  gtnqex  7924  appdivnq  7937  prmuloclemcalc  7939  prmuloc  7940  mullocprlem  7944  ltprordil  7963  ltnqpri  7968  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemlol  7976  ltexprlemopu  7977  ltexprlemupu  7978  ltexprlemdisj  7980  ltexprlemloc  7981  ltexprlemfl  7983  ltexprlemrl  7984  ltexprlemfu  7985  ltexprlemru  7986  ltexpri  7987  recexprlemell  7996  recexprlemelu  7997  recexprlemloc  8005  recexprlempr  8006  recexprlem1ssl  8007  recexprlem1ssu  8008  recexprlemss1l  8009  aptipr  8015  cauappcvgprlemlol  8021  cauappcvgprlemupu  8023  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  cauappcvgprlemladdrl  8031  caucvgprlemnkj  8040  caucvgprlemnbj  8041  caucvgprlemlol  8044  caucvgprlemupu  8046  caucvgprlemladdfu  8051  caucvgprlem1  8053  caucvgprlem2  8054  caucvgprprlemnjltk  8065  caucvgprprlemnbj  8067  caucvgprprlemlol  8072  caucvgprprlemupu  8074  caucvgprprlemexbt  8080  caucvgprprlem1  8083  caucvgprprlem2  8084  suplocexprlemrl  8091  suplocexprlemru  8093  suplocexprlemdisj  8094  suplocexprlemub  8097  suplocexprlemlub  8098  ltsrprg  8121  gt0srpr  8122  recexgt0sr  8147  addgt0sr  8149  mulgt0sr  8152  map2psrprg  8179  suplocsrlemb  8180  suplocsrlem  8182  nnindnn  8267  axcaucvglemcau  8272  axpre-suploclemres  8275  apreap  8924  apreim  8940  mulge0  8956  apti  8959  mulap0bbd  8997  lble  9286  nnind  9330  recnz  9751  uzind  9769  eluzadd  9968  eluzsub  9969  ixxss1  10324  ixxss2  10325  ixxss12  10326  iccss2  10364  iccssioo2  10366  iccssico2  10367  elfzolt2  10582  infssuzcldc  10686  ioom  10713  elicore  10719  flqltp1  10734  flapge  10738  flaplt  10740  addmodlteq  10857  expcl2lemap  11010  expap0i  11030  hashennnuni  11241  hashf1lem2  11309  hashdmprop2dom  11319  wrdexb  11339  swrdsbslen  11461  swrdspsleq  11462  crre  11645  sq01  11683  caucvgre  11770  cvg1nlemcau  11773  cvg1nlemres  11774  resqrexlemoverl  11810  sqrtge0  11822  fimaxre2  12017  climi  12079  reccn2ap  12105  climge0  12117  nnf1o  12169  sumpr  12206  fsump1i  12226  fsum00  12255  fsumparts  12263  mertenslemi1  12328  addsin  12535  subsin  12536  addcos  12539  subcos  12540  sinbnd2  12547  cosbnd2  12548  sinltxirr  12554  dvdsaddre2b  12634  evenelz  12660  4dvdseven  12710  gcd0id  12782  gcd1  12790  bezoutlemstep  12800  dvdsgcdb  12816  mulgcd  12819  gcdzeq  12825  dvdsmulgcd  12828  sqgcd  12832  dvdssqlem  12833  bezoutr  12835  uzwodc  12840  nninfctlemfo  12843  lcmval  12867  lcmcllem  12871  lcmgcdlem  12881  lcmdvds  12883  lcmgcdeq  12887  lcmdvdsb  12888  mulgcddvds  12898  rpmulgcd2  12899  qredeu  12901  rpdvds  12903  divgcdcoprm0  12905  isprm3  12922  divgcdodd  12948  coprm  12949  rpexp  12958  sqrt2irr  12967  qdencl  12995  qeqnumdivden  13000  divnumden  13002  divdenle  13003  densq  13010  phimullem  13033  eulerthlem1  13035  eulerthlemrprm  13037  eulerthlemth  13040  prmdiveq  13044  prmdivdiv  13045  hashgcdeq  13048  phisum  13049  odzid  13053  reumodprminv  13062  oddn2prm  13070  pythagtriplem4  13077  pythagtriplem11  13083  pythagtriplem13  13085  pythagtriplem19  13091  pclemub  13096  pcprendvds2  13100  pcpre1  13101  pcpremul  13102  pceulem  13103  pczdvds  13123  pc2dvds  13139  pcaddlem  13148  pcmpt  13152  pcmpt2  13153  pcmptdvds  13154  pcprod  13155  pockthlem  13165  pockthg  13166  prmunb  13171  1arithlem4  13175  4sqlem7  13193  4sqlem8  13194  4sqlem9  13195  4sqlem10  13196  4sqlemffi  13205  4sqlem15  13214  4sqlem16  13215  4sqlem17  13216  4sqlem18  13217  ballotfilem2  13287  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemi1  13304  ballotfilemii  13305  ballotfilemic  13309  ballotfilem1c  13310  ballotfilemsf1o  13316  ballotfilemscr  13321  ballotfilemrv  13322  ballotfilemfrci  13330  ballotfilemfrceq  13331  ballotfilemrinv0  13335  ennnfonelemom  13358  ennnfonelemex  13364  ennnfonelemf1  13368  ctiunctlemu1st  13384  ctiunctlemu2nd  13385  fnpr2ob  13721  mgmlrid  13759  gzsumfzval  13771  gzsumval2  13774  mndrid  13809  grpinvcnv  13933  dfgrp3mlem  13963  eqglact  14088  ghmgrp2  14109  ghmlin  14111  ghmnsgpreima  14132  kerf1ghm  14137  resscntz  14167  cntzmhm  14174  gzsumsplit0  14239  prdsmndd  14302  prdsgrpd  14305  prdsinvgd  14306  srgdilem  14381  srgdir  14387  srgridm  14392  ringdilem  14424  ringdir  14432  ringridm  14437  unitmulcl  14530  unitnegcl  14547  rhmmhm  14576  elrhmunit  14594  lringuplu  14613  subrgring  14642  subrg1cl  14647  qusrhm  14975  znunit  15104  znrrg  15105  assaassr  15115  assaring  15117  psrbagfsupp  15167  psrbaglecl  15174  psrbagcon  15176  psrbagconcl  15178  gsumbagdiaglem  15180  psrelbas  15184  psrlidmfi  15204  psrridmfi  15205  psrass1fi  15206  mplsubgfilemcl  15227  mplsubgfileminv  15228  inopn  15241  restbasg  15406  ssrest  15420  cntop2  15440  icnpimaex  15449  cnima  15458  lmfss  15482  lmtopcnp  15488  txhmeo  15557  txswaphmeo  15559  psmet0  15565  psmettri2  15566  blhalf  15646  bdxmet  15739  xmetxpbl  15746  ioo2bl  15789  tgioo  15792  cncfi  15816  rescncf  15819  cdivcncfap  15842  cnopnap  15849  divcncfap  15852  dedekindeulemeu  15860  dedekindicclemeu  15869  ivthinclemum  15873  ivthinclemlopn  15874  ivthinclemuopn  15876  ivthinclemdisj  15878  ivthdec  15882  ivthreinc  15883  limcimo  15903  cnplimcim  15905  cnplimclemr  15907  cnlimci  15911  limccnpcntop  15913  limccnp2lem  15914  limccnp2cntop  15915  limccoap  15916  reldvg  15917  dvbsssg  15924  dvfgg  15926  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  dvcjbr  15946  dvrecap  15951  plyco  15997  plycj  15999  plyrecj  16001  sin0pilem1  16020  sin0pilem2  16021  tanrpcl  16076  tangtx  16077  cos0pilt1  16092  logbgcd1irraplemexp  16216  zprmlogbaplem2  16228  zprmlogbaplem3  16229  ppiqsval2  16253  chtqge0  16259  chtqwordi  16275  mpodvdsmulf1o  16296  perfect  16313  bposlem3  16325  bposlem5  16327  bposlem6  16328  bposlem9  16331  lgsne0  16374  lgseisen  16410  lgsquad2lem2  16418  2sqlem8a  16458  2sqlem8  16459  structgrssiedg  16501  uhgrm  16536  umgredgne  16608  usgruspgrben  16644  usgredgppren  16655  umgr2edg  16665  vtxdumgrfival  16756  wlkpropg  16782  wlkv  16784  wlkvtxeledgg  16802  g0wlk0  16828  trlsv  16842  clwwlknlen  16869  eupthv  16904  eupthf1o  16908  eupth2lem3lem4fi  16931  eulerpathprum  16938  bj-charfunbi  17054  bj-inf2vnlem1  17213  pwf1oexmid  17246  subctctexmid  17247  idjudju  17264  iooref1o  17301  taupi  17342  als2d  17353  rals2d  17355  alseu2d  17389  ralseu2d  17391