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  7343  supisoti  7351  djulclb  7396  nninfninc  7464  nnnninfeq2  7470  cardcl  7527  isnumi  7528  cardval3ex  7531  exmidonfinlem  7546  en2eleq  7548  finacn  7561  acfun  7564  exmidaclem  7565  pw1if  7585  papirr  7612  dftap2  7618  exmidapne  7627  ccfunen  7631  acnccim  7639  indpi  7710  dfplpq2  7722  ltbtwnnq  7784  enq0tr  7802  nqnq0pi  7806  elnp1st2nd  7844  prcunqu  7853  prnmaxl  7856  prloc  7859  genpcuu  7888  addnqprllem  7895  addlocprlemeq  7901  addlocprlemgt  7902  addlocpr  7904  nqprxx  7914  gtnqex  7918  appdivnq  7931  prmuloclemcalc  7933  prmuloc  7934  mullocprlem  7938  ltprordil  7957  ltnqpri  7962  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  ltexpri  7981  recexprlemell  7990  recexprlemelu  7991  recexprlemloc  7999  recexprlempr  8000  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  aptipr  8009  cauappcvgprlemlol  8015  cauappcvgprlemupu  8017  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdrl  8025  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemlol  8038  caucvgprlemupu  8040  caucvgprlemladdfu  8045  caucvgprlem1  8047  caucvgprlem2  8048  caucvgprprlemnjltk  8059  caucvgprprlemnbj  8061  caucvgprprlemlol  8066  caucvgprprlemupu  8068  caucvgprprlemexbt  8074  caucvgprprlem1  8077  caucvgprprlem2  8078  suplocexprlemrl  8085  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemub  8091  suplocexprlemlub  8092  ltsrprg  8115  gt0srpr  8116  recexgt0sr  8141  addgt0sr  8143  mulgt0sr  8146  map2psrprg  8173  suplocsrlemb  8174  suplocsrlem  8176  nnindnn  8261  axcaucvglemcau  8266  axpre-suploclemres  8269  apreap  8918  apreim  8934  mulge0  8950  apti  8953  mulap0bbd  8991  lble  9280  nnind  9323  recnz  9744  uzind  9762  eluzadd  9961  eluzsub  9962  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  iccssioo2  10359  iccssico2  10360  elfzolt2  10575  infssuzcldc  10679  ioom  10706  elicore  10712  flqltp1  10727  flapge  10731  addmodlteq  10849  expcl2lemap  11002  expap0i  11022  hashennnuni  11233  hashf1lem2  11301  hashdmprop2dom  11311  wrdexb  11331  swrdsbslen  11453  swrdspsleq  11454  crre  11637  sq01  11675  caucvgre  11762  cvg1nlemcau  11765  cvg1nlemres  11766  resqrexlemoverl  11802  sqrtge0  11814  fimaxre2  12009  climi  12071  reccn2ap  12097  climge0  12109  nnf1o  12161  sumpr  12198  fsump1i  12218  fsum00  12247  fsumparts  12255  mertenslemi1  12320  addsin  12527  subsin  12528  addcos  12531  subcos  12532  sinbnd2  12539  cosbnd2  12540  sinltxirr  12546  dvdsaddre2b  12626  evenelz  12652  4dvdseven  12702  gcd0id  12774  gcd1  12782  bezoutlemstep  12792  dvdsgcdb  12808  mulgcd  12811  gcdzeq  12817  dvdsmulgcd  12820  sqgcd  12824  dvdssqlem  12825  bezoutr  12827  uzwodc  12832  nninfctlemfo  12835  lcmval  12859  lcmcllem  12863  lcmgcdlem  12873  lcmdvds  12875  lcmgcdeq  12879  lcmdvdsb  12880  mulgcddvds  12890  rpmulgcd2  12891  qredeu  12893  rpdvds  12895  divgcdcoprm0  12897  isprm3  12914  divgcdodd  12940  coprm  12941  rpexp  12950  sqrt2irr  12959  qdencl  12987  qeqnumdivden  12992  divnumden  12994  divdenle  12995  densq  13002  phimullem  13025  eulerthlem1  13027  eulerthlemrprm  13029  eulerthlemth  13032  prmdiveq  13036  prmdivdiv  13037  hashgcdeq  13040  phisum  13041  odzid  13045  reumodprminv  13054  oddn2prm  13062  pythagtriplem4  13069  pythagtriplem11  13075  pythagtriplem13  13077  pythagtriplem19  13083  pclemub  13088  pcprendvds2  13092  pcpre1  13093  pcpremul  13094  pceulem  13095  pczdvds  13115  pc2dvds  13131  pcaddlem  13140  pcmpt  13144  pcmpt2  13145  pcmptdvds  13146  pcprod  13147  pockthlem  13157  pockthg  13158  prmunb  13163  1arithlem4  13167  4sqlem7  13185  4sqlem8  13186  4sqlem9  13187  4sqlem10  13188  4sqlemffi  13197  4sqlem15  13206  4sqlem16  13207  4sqlem17  13208  4sqlem18  13209  ballotfilem2  13279  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemi1  13296  ballotfilemii  13297  ballotfilemic  13301  ballotfilem1c  13302  ballotfilemsf1o  13308  ballotfilemscr  13313  ballotfilemrv  13314  ballotfilemfrci  13322  ballotfilemfrceq  13323  ballotfilemrinv0  13327  ennnfonelemom  13350  ennnfonelemex  13356  ennnfonelemf1  13360  ctiunctlemu1st  13376  ctiunctlemu2nd  13377  fnpr2ob  13712  mgmlrid  13750  gzsumfzval  13762  gzsumval2  13765  mndrid  13800  grpinvcnv  13924  dfgrp3mlem  13954  eqglact  14079  ghmgrp2  14100  ghmlin  14102  ghmnsgpreima  14123  kerf1ghm  14128  gzsumsplit0  14199  prdsmndd  14245  prdsgrpd  14248  prdsinvgd  14249  srgdilem  14324  srgdir  14330  srgridm  14335  ringdilem  14367  ringdir  14375  ringridm  14380  unitmulcl  14471  unitnegcl  14488  rhmmhm  14517  elrhmunit  14535  lringuplu  14554  subrgring  14583  subrg1cl  14588  qusrhm  14916  znunit  15045  znrrg  15046  assaassr  15056  assaring  15058  psrbagfsupp  15106  psrbaglecl  15111  psrbagcon  15113  psrbagconcl  15115  psrelbas  15118  mplsubgfilemcl  15142  mplsubgfileminv  15143  inopn  15156  restbasg  15321  ssrest  15335  cntop2  15355  icnpimaex  15364  cnima  15373  lmfss  15397  lmtopcnp  15403  txhmeo  15472  txswaphmeo  15474  psmet0  15480  psmettri2  15481  blhalf  15561  bdxmet  15654  xmetxpbl  15661  ioo2bl  15704  tgioo  15707  cncfi  15731  rescncf  15734  cdivcncfap  15757  cnopnap  15764  divcncfap  15767  dedekindeulemeu  15775  dedekindicclemeu  15784  ivthinclemum  15788  ivthinclemlopn  15789  ivthinclemuopn  15791  ivthinclemdisj  15793  ivthdec  15797  ivthreinc  15798  limcimo  15818  cnplimcim  15820  cnplimclemr  15822  cnlimci  15826  limccnpcntop  15828  limccnp2lem  15829  limccnp2cntop  15830  limccoap  15831  reldvg  15832  dvbsssg  15839  dvfgg  15841  dvaddxxbr  15854  dvmulxxbr  15855  dvcoapbr  15860  dvcjbr  15861  dvrecap  15866  plyco  15912  plycj  15914  plyrecj  15916  sin0pilem1  15935  sin0pilem2  15936  tanrpcl  15991  tangtx  15992  cos0pilt1  16006  logbgcd1irraplemexp  16126  zprmlogbaplem2  16138  zprmlogbaplem3  16139  ppiqsval2  16163  chtqge0  16169  chtqwordi  16185  mpodvdsmulf1o  16206  perfect  16223  bposlem3  16235  bposlem5  16237  lgsne0  16279  lgseisen  16315  lgsquad2lem2  16323  2sqlem8a  16363  2sqlem8  16364  structgrssiedg  16406  uhgrm  16441  umgredgne  16513  usgruspgrben  16549  usgredgppren  16560  umgr2edg  16570  vtxdumgrfival  16661  wlkpropg  16687  wlkv  16689  wlkvtxeledgg  16707  g0wlk0  16733  trlsv  16747  clwwlknlen  16774  eupthv  16809  eupthf1o  16813  eupth2lem3lem4fi  16836  eulerpathprum  16843  bj-charfunbi  16959  bj-inf2vnlem1  17118  pwf1oexmid  17151  subctctexmid  17152  iooref1o  17205  taupi  17245  als2d  17256  rals2d  17258  alseu2d  17292  ralseu2d  17294