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  simprld  530  simprrd  532  simp2  1003  simp3  1004  sbh  1802  eldifbd  3189  unssbd  3362  opth  4302  potr  4376  frind  4420  brrelex2  4737  funinsn  5346  feu  5484  fcnvres  5485  fun11iun  5569  funopsn  5790  elmpocl2  6173  uchoice  6253  oprssdmm  6287  tfrlem1  6424  tfrlemisucfn  6440  tfrlemisucaccv  6441  tfrlemibxssdm  6443  tfrlemibfn  6444  tfrlemi14d  6449  swoer  6678  elmapssres  6790  mapsspm  6799  pmsspw  6800  mapss  6808  dom0  6967  xpf1o  6973  sbthlemi8  7099  sbthlemi9  7100  supelti  7137  supisoti  7145  djulclb  7190  nninfninc  7258  nnnninfeq2  7264  cardcl  7321  isnumi  7322  cardval3ex  7325  exmidonfinlem  7339  en2eleq  7341  finacn  7354  acfun  7357  exmidaclem  7358  pw1if  7378  dftap2  7405  exmidapne  7414  ccfunen  7418  acnccim  7426  indpi  7497  dfplpq2  7509  ltbtwnnq  7571  enq0tr  7589  nqnq0pi  7593  elnp1st2nd  7631  prcunqu  7640  prnmaxl  7643  prloc  7646  genpcuu  7675  addnqprllem  7682  addlocprlemeq  7688  addlocprlemgt  7689  addlocpr  7691  nqprxx  7701  gtnqex  7705  appdivnq  7718  prmuloclemcalc  7720  prmuloc  7721  mullocprlem  7725  ltprordil  7744  ltnqpri  7749  ltexprlemm  7755  ltexprlemopl  7756  ltexprlemlol  7757  ltexprlemopu  7758  ltexprlemupu  7759  ltexprlemdisj  7761  ltexprlemloc  7762  ltexprlemfl  7764  ltexprlemrl  7765  ltexprlemfu  7766  ltexprlemru  7767  ltexpri  7768  recexprlemell  7777  recexprlemelu  7778  recexprlemloc  7786  recexprlempr  7787  recexprlem1ssl  7788  recexprlem1ssu  7789  recexprlemss1l  7790  aptipr  7796  cauappcvgprlemlol  7802  cauappcvgprlemupu  7804  cauappcvgprlemladdfu  7809  cauappcvgprlemladdfl  7810  cauappcvgprlemladdrl  7812  caucvgprlemnkj  7821  caucvgprlemnbj  7822  caucvgprlemlol  7825  caucvgprlemupu  7827  caucvgprlemladdfu  7832  caucvgprlem1  7834  caucvgprlem2  7835  caucvgprprlemnjltk  7846  caucvgprprlemnbj  7848  caucvgprprlemlol  7853  caucvgprprlemupu  7855  caucvgprprlemexbt  7861  caucvgprprlem1  7864  caucvgprprlem2  7865  suplocexprlemrl  7872  suplocexprlemru  7874  suplocexprlemdisj  7875  suplocexprlemub  7878  suplocexprlemlub  7879  ltsrprg  7902  gt0srpr  7903  recexgt0sr  7928  addgt0sr  7930  mulgt0sr  7933  map2psrprg  7960  suplocsrlemb  7961  suplocsrlem  7963  nnindnn  8048  axcaucvglemcau  8053  axpre-suploclemres  8056  apreap  8702  apreim  8718  mulge0  8734  apti  8737  mulap0bbd  8775  lble  9062  nnind  9094  recnz  9508  uzind  9526  eluzadd  9719  eluzsub  9720  ixxss1  10068  ixxss2  10069  ixxss12  10070  iccss2  10108  iccssioo2  10110  iccssico2  10111  elfzolt2  10321  infssuzcldc  10422  ioom  10447  elicore  10453  flqltp1  10466  addmodlteq  10587  expcl2lemap  10740  expap0i  10760  hashennnuni  10968  hashdmprop2dom  11033  wrdexb  11050  swrdsbslen  11164  swrdspsleq  11165  crre  11334  caucvgre  11458  cvg1nlemcau  11461  cvg1nlemres  11462  resqrexlemoverl  11498  sqrtge0  11510  fimaxre2  11704  climi  11764  reccn2ap  11790  climge0  11802  nnf1o  11853  sumpr  11890  fsump1i  11910  fsum00  11939  fsumparts  11947  mertenslemi1  12012  addsin  12219  subsin  12220  addcos  12223  subcos  12224  sinbnd2  12231  cosbnd2  12232  sinltxirr  12238  dvdsaddre2b  12318  evenelz  12344  4dvdseven  12394  gcd0id  12466  gcd1  12474  bezoutlemstep  12484  dvdsgcdb  12500  mulgcd  12503  gcdzeq  12509  dvdsmulgcd  12512  sqgcd  12516  dvdssqlem  12517  bezoutr  12519  uzwodc  12524  nninfctlemfo  12527  lcmval  12551  lcmcllem  12555  lcmgcdlem  12565  lcmdvds  12567  lcmgcdeq  12571  lcmdvdsb  12572  mulgcddvds  12582  rpmulgcd2  12583  qredeu  12585  rpdvds  12587  divgcdcoprm0  12589  isprm3  12606  divgcdodd  12631  coprm  12632  rpexp  12641  sqrt2irr  12650  qdencl  12677  qeqnumdivden  12682  divnumden  12684  divdenle  12685  densq  12692  phimullem  12713  eulerthlem1  12715  eulerthlemrprm  12717  eulerthlemth  12720  prmdiveq  12724  prmdivdiv  12725  hashgcdeq  12728  phisum  12729  odzid  12733  reumodprminv  12742  oddn2prm  12750  pythagtriplem4  12757  pythagtriplem11  12763  pythagtriplem13  12765  pythagtriplem19  12771  pclemub  12776  pcprendvds2  12780  pcpre1  12781  pcpremul  12782  pceulem  12783  pczdvds  12803  pc2dvds  12819  pcaddlem  12828  pcmpt  12832  pcmpt2  12833  pcmptdvds  12834  pcprod  12835  pockthlem  12845  pockthg  12846  prmunb  12851  1arithlem4  12855  4sqlem7  12873  4sqlem8  12874  4sqlem9  12875  4sqlem10  12876  4sqlemffi  12885  4sqlem15  12894  4sqlem16  12895  4sqlem17  12896  4sqlem18  12897  ennnfonelemom  12945  ennnfonelemex  12951  ennnfonelemf1  12955  ctiunctlemu1st  12971  ctiunctlemu2nd  12972  fnpr2ob  13339  mgmlrid  13378  gsumfzval  13390  gsumval2  13396  mndrid  13435  prdsmndd  13447  grpinvcnv  13567  dfgrp3mlem  13597  prdsgrpd  13608  prdsinvgd  13609  eqglact  13728  ghmgrp2  13749  ghmlin  13751  ghmnsgpreima  13772  kerf1ghm  13777  srgdilem  13898  srgdir  13904  srgridm  13909  ringdilem  13941  ringdir  13948  ringridm  13953  unitmulcl  14042  unitnegcl  14059  rhmmhm  14088  elrhmunit  14106  lringuplu  14125  subrgring  14153  subrg1cl  14158  qusrhm  14457  znunit  14588  znrrg  14589  psrelbas  14604  mplsubgfilemcl  14628  mplsubgfileminv  14629  inopn  14642  restbasg  14807  ssrest  14821  cntop2  14841  icnpimaex  14850  cnima  14859  lmfss  14883  lmtopcnp  14889  txhmeo  14958  txswaphmeo  14960  psmet0  14966  psmettri2  14967  blhalf  15047  bdxmet  15140  xmetxpbl  15147  ioo2bl  15190  tgioo  15193  cncfi  15217  rescncf  15220  cdivcncfap  15243  cnopnap  15250  divcncfap  15253  dedekindeulemeu  15261  dedekindicclemeu  15270  ivthinclemum  15274  ivthinclemlopn  15275  ivthinclemuopn  15277  ivthinclemdisj  15279  ivthdec  15283  ivthreinc  15284  limcimo  15304  cnplimcim  15306  cnplimclemr  15308  cnlimci  15312  limccnpcntop  15314  limccnp2lem  15315  limccnp2cntop  15316  limccoap  15317  reldvg  15318  dvbsssg  15325  dvfgg  15327  dvaddxxbr  15340  dvmulxxbr  15341  dvcoapbr  15346  dvcjbr  15347  dvrecap  15352  plyco  15398  plycj  15400  plyrecj  15402  sin0pilem1  15420  sin0pilem2  15421  tanrpcl  15476  tangtx  15477  cos0pilt1  15491  logbgcd1irraplemexp  15607  mpodvdsmulf1o  15629  perfect  15640  lgsne0  15682  lgseisen  15718  lgsquad2lem2  15726  2sqlem8a  15766  2sqlem8  15767  structgrssiedg  15809  uhgrm  15843  umgredgne  15913  usgruspgrben  15949  usgredgppren  15960  umgr2edg  15970  bj-charfunbi  16084  bj-inf2vnlem1  16243  pwf1oexmid  16276  subctctexmid  16277  iooref1o  16313  taupi  16352  alsi2d  16361  alsc2d  16363