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  1022  simp3  1023  sbh  1822  eldifbd  3209  unssbd  3382  opth  4324  potr  4400  frind  4444  brrelex2  4762  funinsn  5373  feu  5513  fcnvres  5514  fun11iun  5598  funopsn  5822  elmpocl2  6211  uchoice  6292  oprssdmm  6326  tfrlem1  6465  tfrlemisucfn  6481  tfrlemisucaccv  6482  tfrlemibxssdm  6484  tfrlemibfn  6485  tfrlemi14d  6490  swoer  6721  elmapssres  6833  mapsspm  6842  pmsspw  6843  mapss  6851  dom0  7012  xpf1o  7018  sbthlemi8  7147  sbthlemi9  7148  supelti  7185  supisoti  7193  djulclb  7238  nninfninc  7306  nnnninfeq2  7312  cardcl  7369  isnumi  7370  cardval3ex  7373  exmidonfinlem  7387  en2eleq  7389  finacn  7402  acfun  7405  exmidaclem  7406  pw1if  7426  dftap2  7453  exmidapne  7462  ccfunen  7466  acnccim  7474  indpi  7545  dfplpq2  7557  ltbtwnnq  7619  enq0tr  7637  nqnq0pi  7641  elnp1st2nd  7679  prcunqu  7688  prnmaxl  7691  prloc  7694  genpcuu  7723  addnqprllem  7730  addlocprlemeq  7736  addlocprlemgt  7737  addlocpr  7739  nqprxx  7749  gtnqex  7753  appdivnq  7766  prmuloclemcalc  7768  prmuloc  7769  mullocprlem  7773  ltprordil  7792  ltnqpri  7797  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemlol  7805  ltexprlemopu  7806  ltexprlemupu  7807  ltexprlemdisj  7809  ltexprlemloc  7810  ltexprlemfl  7812  ltexprlemrl  7813  ltexprlemfu  7814  ltexprlemru  7815  ltexpri  7816  recexprlemell  7825  recexprlemelu  7826  recexprlemloc  7834  recexprlempr  7835  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1l  7838  aptipr  7844  cauappcvgprlemlol  7850  cauappcvgprlemupu  7852  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  cauappcvgprlemladdrl  7860  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemlol  7873  caucvgprlemupu  7875  caucvgprlemladdfu  7880  caucvgprlem1  7882  caucvgprlem2  7883  caucvgprprlemnjltk  7894  caucvgprprlemnbj  7896  caucvgprprlemlol  7901  caucvgprprlemupu  7903  caucvgprprlemexbt  7909  caucvgprprlem1  7912  caucvgprprlem2  7913  suplocexprlemrl  7920  suplocexprlemru  7922  suplocexprlemdisj  7923  suplocexprlemub  7926  suplocexprlemlub  7927  ltsrprg  7950  gt0srpr  7951  recexgt0sr  7976  addgt0sr  7978  mulgt0sr  7981  map2psrprg  8008  suplocsrlemb  8009  suplocsrlem  8011  nnindnn  8096  axcaucvglemcau  8101  axpre-suploclemres  8104  apreap  8750  apreim  8766  mulge0  8782  apti  8785  mulap0bbd  8823  lble  9110  nnind  9142  recnz  9556  uzind  9574  eluzadd  9768  eluzsub  9769  ixxss1  10117  ixxss2  10118  ixxss12  10119  iccss2  10157  iccssioo2  10159  iccssico2  10160  elfzolt2  10370  infssuzcldc  10472  ioom  10497  elicore  10503  flqltp1  10516  addmodlteq  10637  expcl2lemap  10790  expap0i  10810  hashennnuni  11018  hashdmprop2dom  11084  wrdexb  11101  swrdsbslen  11219  swrdspsleq  11220  crre  11389  caucvgre  11513  cvg1nlemcau  11516  cvg1nlemres  11517  resqrexlemoverl  11553  sqrtge0  11565  fimaxre2  11759  climi  11819  reccn2ap  11845  climge0  11857  nnf1o  11908  sumpr  11945  fsump1i  11965  fsum00  11994  fsumparts  12002  mertenslemi1  12067  addsin  12274  subsin  12275  addcos  12278  subcos  12279  sinbnd2  12286  cosbnd2  12287  sinltxirr  12293  dvdsaddre2b  12373  evenelz  12399  4dvdseven  12449  gcd0id  12521  gcd1  12529  bezoutlemstep  12539  dvdsgcdb  12555  mulgcd  12558  gcdzeq  12564  dvdsmulgcd  12567  sqgcd  12571  dvdssqlem  12572  bezoutr  12574  uzwodc  12579  nninfctlemfo  12582  lcmval  12606  lcmcllem  12610  lcmgcdlem  12620  lcmdvds  12622  lcmgcdeq  12626  lcmdvdsb  12627  mulgcddvds  12637  rpmulgcd2  12638  qredeu  12640  rpdvds  12642  divgcdcoprm0  12644  isprm3  12661  divgcdodd  12686  coprm  12687  rpexp  12696  sqrt2irr  12705  qdencl  12732  qeqnumdivden  12737  divnumden  12739  divdenle  12740  densq  12747  phimullem  12768  eulerthlem1  12770  eulerthlemrprm  12772  eulerthlemth  12775  prmdiveq  12779  prmdivdiv  12780  hashgcdeq  12783  phisum  12784  odzid  12788  reumodprminv  12797  oddn2prm  12805  pythagtriplem4  12812  pythagtriplem11  12818  pythagtriplem13  12820  pythagtriplem19  12826  pclemub  12831  pcprendvds2  12835  pcpre1  12836  pcpremul  12837  pceulem  12838  pczdvds  12858  pc2dvds  12874  pcaddlem  12883  pcmpt  12887  pcmpt2  12888  pcmptdvds  12889  pcprod  12890  pockthlem  12900  pockthg  12901  prmunb  12906  1arithlem4  12910  4sqlem7  12928  4sqlem8  12929  4sqlem9  12930  4sqlem10  12931  4sqlemffi  12940  4sqlem15  12949  4sqlem16  12950  4sqlem17  12951  4sqlem18  12952  ennnfonelemom  13000  ennnfonelemex  13006  ennnfonelemf1  13010  ctiunctlemu1st  13026  ctiunctlemu2nd  13027  fnpr2ob  13394  mgmlrid  13433  gsumfzval  13445  gsumval2  13451  mndrid  13490  prdsmndd  13502  grpinvcnv  13622  dfgrp3mlem  13652  prdsgrpd  13663  prdsinvgd  13664  eqglact  13783  ghmgrp2  13804  ghmlin  13806  ghmnsgpreima  13827  kerf1ghm  13832  srgdilem  13953  srgdir  13959  srgridm  13964  ringdilem  13996  ringdir  14003  ringridm  14008  unitmulcl  14098  unitnegcl  14115  rhmmhm  14144  elrhmunit  14162  lringuplu  14181  subrgring  14209  subrg1cl  14214  qusrhm  14513  znunit  14644  znrrg  14645  psrelbas  14660  mplsubgfilemcl  14684  mplsubgfileminv  14685  inopn  14698  restbasg  14863  ssrest  14877  cntop2  14897  icnpimaex  14906  cnima  14915  lmfss  14939  lmtopcnp  14945  txhmeo  15014  txswaphmeo  15016  psmet0  15022  psmettri2  15023  blhalf  15103  bdxmet  15196  xmetxpbl  15203  ioo2bl  15246  tgioo  15249  cncfi  15273  rescncf  15276  cdivcncfap  15299  cnopnap  15306  divcncfap  15309  dedekindeulemeu  15317  dedekindicclemeu  15326  ivthinclemum  15330  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthinclemdisj  15335  ivthdec  15339  ivthreinc  15340  limcimo  15360  cnplimcim  15362  cnplimclemr  15364  cnlimci  15368  limccnpcntop  15370  limccnp2lem  15371  limccnp2cntop  15372  limccoap  15373  reldvg  15374  dvbsssg  15381  dvfgg  15383  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvcjbr  15403  dvrecap  15408  plyco  15454  plycj  15456  plyrecj  15458  sin0pilem1  15476  sin0pilem2  15477  tanrpcl  15532  tangtx  15533  cos0pilt1  15547  logbgcd1irraplemexp  15663  mpodvdsmulf1o  15685  perfect  15696  lgsne0  15738  lgseisen  15774  lgsquad2lem2  15782  2sqlem8a  15822  2sqlem8  15823  structgrssiedg  15865  uhgrm  15899  umgredgne  15969  usgruspgrben  16005  usgredgppren  16016  umgr2edg  16026  vtxdumgrfival  16084  wlkpropg  16096  wlkv  16098  wlkvtxeledgg  16116  g0wlk0  16142  trlsv  16154  clwwlknlen  16180  bj-charfunbi  16283  bj-inf2vnlem1  16442  pwf1oexmid  16478  subctctexmid  16479  iooref1o  16516  taupi  16555  alsi2d  16564  alsc2d  16566