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  4377  potr  4453  frind  4497  brrelex2  4816  funinsn  5430  feu  5574  fcnvres  5575  fun11iun  5660  funopsn  5891  elmpocl2  6286  uchoice  6371  oprssdmm  6405  fczsupp0  6499  tfrlem1  6579  tfrlemisucfn  6595  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi14d  6604  swoer  6835  elmapssres  6954  mapsspm  6963  pmsspw  6964  mapss  6973  dom0  7138  xpf1o  7144  sbthlemi8  7281  sbthlemi9  7282  fsuppimpd  7293  supelti  7342  supisoti  7350  djulclb  7395  nninfninc  7463  nnnninfeq2  7469  cardcl  7526  isnumi  7527  cardval3ex  7530  exmidonfinlem  7545  en2eleq  7547  finacn  7560  acfun  7563  exmidaclem  7564  pw1if  7584  papirr  7611  dftap2  7617  exmidapne  7626  ccfunen  7630  acnccim  7638  indpi  7709  dfplpq2  7721  ltbtwnnq  7783  enq0tr  7801  nqnq0pi  7805  elnp1st2nd  7843  prcunqu  7852  prnmaxl  7855  prloc  7858  genpcuu  7887  addnqprllem  7894  addlocprlemeq  7900  addlocprlemgt  7901  addlocpr  7903  nqprxx  7913  gtnqex  7917  appdivnq  7930  prmuloclemcalc  7932  prmuloc  7933  mullocprlem  7937  ltprordil  7956  ltnqpri  7961  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltexpri  7980  recexprlemell  7989  recexprlemelu  7990  recexprlemloc  7998  recexprlempr  7999  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  aptipr  8008  cauappcvgprlemlol  8014  cauappcvgprlemupu  8016  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdrl  8024  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemlol  8037  caucvgprlemupu  8039  caucvgprlemladdfu  8044  caucvgprlem1  8046  caucvgprlem2  8047  caucvgprprlemnjltk  8058  caucvgprprlemnbj  8060  caucvgprprlemlol  8065  caucvgprprlemupu  8067  caucvgprprlemexbt  8073  caucvgprprlem1  8076  caucvgprprlem2  8077  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemub  8090  suplocexprlemlub  8091  ltsrprg  8114  gt0srpr  8115  recexgt0sr  8140  addgt0sr  8142  mulgt0sr  8145  map2psrprg  8172  suplocsrlemb  8173  suplocsrlem  8175  nnindnn  8260  axcaucvglemcau  8265  axpre-suploclemres  8268  apreap  8916  apreim  8932  mulge0  8948  apti  8951  mulap0bbd  8989  lble  9278  nnind  9321  recnz  9741  uzind  9759  eluzadd  9953  eluzsub  9954  ixxss1  10308  ixxss2  10309  ixxss12  10310  iccss2  10348  iccssioo2  10350  iccssico2  10351  elfzolt2  10566  infssuzcldc  10670  ioom  10697  elicore  10703  flqltp1  10716  addmodlteq  10837  expcl2lemap  10990  expap0i  11010  hashennnuni  11220  hashf1lem2  11288  hashdmprop2dom  11298  wrdexb  11318  swrdsbslen  11440  swrdspsleq  11441  crre  11624  sq01  11662  caucvgre  11749  cvg1nlemcau  11752  cvg1nlemres  11753  resqrexlemoverl  11789  sqrtge0  11801  fimaxre2  11995  climi  12055  reccn2ap  12081  climge0  12093  nnf1o  12145  sumpr  12182  fsump1i  12202  fsum00  12231  fsumparts  12239  mertenslemi1  12304  addsin  12511  subsin  12512  addcos  12515  subcos  12516  sinbnd2  12523  cosbnd2  12524  sinltxirr  12530  dvdsaddre2b  12610  evenelz  12636  4dvdseven  12686  gcd0id  12758  gcd1  12766  bezoutlemstep  12776  dvdsgcdb  12792  mulgcd  12795  gcdzeq  12801  dvdsmulgcd  12804  sqgcd  12808  dvdssqlem  12809  bezoutr  12811  uzwodc  12816  nninfctlemfo  12819  lcmval  12843  lcmcllem  12847  lcmgcdlem  12857  lcmdvds  12859  lcmgcdeq  12863  lcmdvdsb  12864  mulgcddvds  12874  rpmulgcd2  12875  qredeu  12877  rpdvds  12879  divgcdcoprm0  12881  isprm3  12898  divgcdodd  12923  coprm  12924  rpexp  12933  sqrt2irr  12942  qdencl  12969  qeqnumdivden  12974  divnumden  12976  divdenle  12977  densq  12984  phimullem  13005  eulerthlem1  13007  eulerthlemrprm  13009  eulerthlemth  13012  prmdiveq  13016  prmdivdiv  13017  hashgcdeq  13020  phisum  13021  odzid  13025  reumodprminv  13034  oddn2prm  13042  pythagtriplem4  13049  pythagtriplem11  13055  pythagtriplem13  13057  pythagtriplem19  13063  pclemub  13068  pcprendvds2  13072  pcpre1  13073  pcpremul  13074  pceulem  13075  pczdvds  13095  pc2dvds  13111  pcaddlem  13120  pcmpt  13124  pcmpt2  13125  pcmptdvds  13126  pcprod  13127  pockthlem  13137  pockthg  13138  prmunb  13143  1arithlem4  13147  4sqlem7  13165  4sqlem8  13166  4sqlem9  13167  4sqlem10  13168  4sqlemffi  13177  4sqlem15  13186  4sqlem16  13187  4sqlem17  13188  4sqlem18  13189  ballotfilem2  13230  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemi1  13247  ballotfilemii  13248  ballotfilemic  13252  ballotfilem1c  13253  ballotfilemsf1o  13259  ballotfilemscr  13264  ballotfilemrv  13265  ballotfilemfrci  13273  ballotfilemfrceq  13274  ballotfilemrinv0  13278  ennnfonelemom  13301  ennnfonelemex  13307  ennnfonelemf1  13311  ctiunctlemu1st  13327  ctiunctlemu2nd  13328  fnpr2ob  13663  mgmlrid  13701  gzsumfzval  13713  gzsumval2  13716  mndrid  13751  grpinvcnv  13875  dfgrp3mlem  13905  eqglact  14030  ghmgrp2  14051  ghmlin  14053  ghmnsgpreima  14074  kerf1ghm  14079  gzsumsplit0  14150  prdsmndd  14196  prdsgrpd  14199  prdsinvgd  14200  srgdilem  14275  srgdir  14281  srgridm  14286  ringdilem  14318  ringdir  14326  ringridm  14331  unitmulcl  14422  unitnegcl  14439  rhmmhm  14468  elrhmunit  14486  lringuplu  14505  subrgring  14534  subrg1cl  14539  qusrhm  14867  znunit  14996  znrrg  14997  assaassr  15007  assaring  15009  psrbagfsupp  15057  psrbaglecl  15062  psrbagcon  15064  psrbagconcl  15065  psrelbas  15068  mplsubgfilemcl  15092  mplsubgfileminv  15093  inopn  15106  restbasg  15271  ssrest  15285  cntop2  15305  icnpimaex  15314  cnima  15323  lmfss  15347  lmtopcnp  15353  txhmeo  15422  txswaphmeo  15424  psmet0  15430  psmettri2  15431  blhalf  15511  bdxmet  15604  xmetxpbl  15611  ioo2bl  15654  tgioo  15657  cncfi  15681  rescncf  15684  cdivcncfap  15707  cnopnap  15714  divcncfap  15717  dedekindeulemeu  15725  dedekindicclemeu  15734  ivthinclemum  15738  ivthinclemlopn  15739  ivthinclemuopn  15741  ivthinclemdisj  15743  ivthdec  15747  ivthreinc  15748  limcimo  15768  cnplimcim  15770  cnplimclemr  15772  cnlimci  15776  limccnpcntop  15778  limccnp2lem  15779  limccnp2cntop  15780  limccoap  15781  reldvg  15782  dvbsssg  15789  dvfgg  15791  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  dvcjbr  15811  dvrecap  15816  plyco  15862  plycj  15864  plyrecj  15866  sin0pilem1  15885  sin0pilem2  15886  tanrpcl  15941  tangtx  15942  cos0pilt1  15956  logbgcd1irraplemexp  16076  mpodvdsmulf1o  16110  perfect  16121  lgsne0  16169  lgseisen  16205  lgsquad2lem2  16213  2sqlem8a  16253  2sqlem8  16254  structgrssiedg  16296  uhgrm  16331  umgredgne  16403  usgruspgrben  16439  usgredgppren  16450  umgr2edg  16460  vtxdumgrfival  16551  wlkpropg  16577  wlkv  16579  wlkvtxeledgg  16597  g0wlk0  16623  trlsv  16637  clwwlknlen  16664  eupthv  16699  eupthf1o  16703  eupth2lem3lem4fi  16726  eulerpathprum  16733  bj-charfunbi  16849  bj-inf2vnlem1  17008  pwf1oexmid  17041  subctctexmid  17042  iooref1o  17095  taupi  17135  als2d  17146  rals2d  17148  alseu2d  17182  ralseu2d  17184