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  4323  potr  4399  frind  4443  brrelex2  4760  funinsn  5370  feu  5510  fcnvres  5511  fun11iun  5595  funopsn  5819  elmpocl2  6208  uchoice  6289  oprssdmm  6323  tfrlem1  6460  tfrlemisucfn  6476  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemi14d  6485  swoer  6716  elmapssres  6828  mapsspm  6837  pmsspw  6838  mapss  6846  dom0  7007  xpf1o  7013  sbthlemi8  7139  sbthlemi9  7140  supelti  7177  supisoti  7185  djulclb  7230  nninfninc  7298  nnnninfeq2  7304  cardcl  7361  isnumi  7362  cardval3ex  7365  exmidonfinlem  7379  en2eleq  7381  finacn  7394  acfun  7397  exmidaclem  7398  pw1if  7418  dftap2  7445  exmidapne  7454  ccfunen  7458  acnccim  7466  indpi  7537  dfplpq2  7549  ltbtwnnq  7611  enq0tr  7629  nqnq0pi  7633  elnp1st2nd  7671  prcunqu  7680  prnmaxl  7683  prloc  7686  genpcuu  7715  addnqprllem  7722  addlocprlemeq  7728  addlocprlemgt  7729  addlocpr  7731  nqprxx  7741  gtnqex  7745  appdivnq  7758  prmuloclemcalc  7760  prmuloc  7761  mullocprlem  7765  ltprordil  7784  ltnqpri  7789  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemlol  7797  ltexprlemopu  7798  ltexprlemupu  7799  ltexprlemdisj  7801  ltexprlemloc  7802  ltexprlemfl  7804  ltexprlemrl  7805  ltexprlemfu  7806  ltexprlemru  7807  ltexpri  7808  recexprlemell  7817  recexprlemelu  7818  recexprlemloc  7826  recexprlempr  7827  recexprlem1ssl  7828  recexprlem1ssu  7829  recexprlemss1l  7830  aptipr  7836  cauappcvgprlemlol  7842  cauappcvgprlemupu  7844  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  cauappcvgprlemladdrl  7852  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemlol  7865  caucvgprlemupu  7867  caucvgprlemladdfu  7872  caucvgprlem1  7874  caucvgprlem2  7875  caucvgprprlemnjltk  7886  caucvgprprlemnbj  7888  caucvgprprlemlol  7893  caucvgprprlemupu  7895  caucvgprprlemexbt  7901  caucvgprprlem1  7904  caucvgprprlem2  7905  suplocexprlemrl  7912  suplocexprlemru  7914  suplocexprlemdisj  7915  suplocexprlemub  7918  suplocexprlemlub  7919  ltsrprg  7942  gt0srpr  7943  recexgt0sr  7968  addgt0sr  7970  mulgt0sr  7973  map2psrprg  8000  suplocsrlemb  8001  suplocsrlem  8003  nnindnn  8088  axcaucvglemcau  8093  axpre-suploclemres  8096  apreap  8742  apreim  8758  mulge0  8774  apti  8777  mulap0bbd  8815  lble  9102  nnind  9134  recnz  9548  uzind  9566  eluzadd  9759  eluzsub  9760  ixxss1  10108  ixxss2  10109  ixxss12  10110  iccss2  10148  iccssioo2  10150  iccssico2  10151  elfzolt2  10361  infssuzcldc  10463  ioom  10488  elicore  10494  flqltp1  10507  addmodlteq  10628  expcl2lemap  10781  expap0i  10801  hashennnuni  11009  hashdmprop2dom  11074  wrdexb  11091  swrdsbslen  11206  swrdspsleq  11207  crre  11376  caucvgre  11500  cvg1nlemcau  11503  cvg1nlemres  11504  resqrexlemoverl  11540  sqrtge0  11552  fimaxre2  11746  climi  11806  reccn2ap  11832  climge0  11844  nnf1o  11895  sumpr  11932  fsump1i  11952  fsum00  11981  fsumparts  11989  mertenslemi1  12054  addsin  12261  subsin  12262  addcos  12265  subcos  12266  sinbnd2  12273  cosbnd2  12274  sinltxirr  12280  dvdsaddre2b  12360  evenelz  12386  4dvdseven  12436  gcd0id  12508  gcd1  12516  bezoutlemstep  12526  dvdsgcdb  12542  mulgcd  12545  gcdzeq  12551  dvdsmulgcd  12554  sqgcd  12558  dvdssqlem  12559  bezoutr  12561  uzwodc  12566  nninfctlemfo  12569  lcmval  12593  lcmcllem  12597  lcmgcdlem  12607  lcmdvds  12609  lcmgcdeq  12613  lcmdvdsb  12614  mulgcddvds  12624  rpmulgcd2  12625  qredeu  12627  rpdvds  12629  divgcdcoprm0  12631  isprm3  12648  divgcdodd  12673  coprm  12674  rpexp  12683  sqrt2irr  12692  qdencl  12719  qeqnumdivden  12724  divnumden  12726  divdenle  12727  densq  12734  phimullem  12755  eulerthlem1  12757  eulerthlemrprm  12759  eulerthlemth  12762  prmdiveq  12766  prmdivdiv  12767  hashgcdeq  12770  phisum  12771  odzid  12775  reumodprminv  12784  oddn2prm  12792  pythagtriplem4  12799  pythagtriplem11  12805  pythagtriplem13  12807  pythagtriplem19  12813  pclemub  12818  pcprendvds2  12822  pcpre1  12823  pcpremul  12824  pceulem  12825  pczdvds  12845  pc2dvds  12861  pcaddlem  12870  pcmpt  12874  pcmpt2  12875  pcmptdvds  12876  pcprod  12877  pockthlem  12887  pockthg  12888  prmunb  12893  1arithlem4  12897  4sqlem7  12915  4sqlem8  12916  4sqlem9  12917  4sqlem10  12918  4sqlemffi  12927  4sqlem15  12936  4sqlem16  12937  4sqlem17  12938  4sqlem18  12939  ennnfonelemom  12987  ennnfonelemex  12993  ennnfonelemf1  12997  ctiunctlemu1st  13013  ctiunctlemu2nd  13014  fnpr2ob  13381  mgmlrid  13420  gsumfzval  13432  gsumval2  13438  mndrid  13477  prdsmndd  13489  grpinvcnv  13609  dfgrp3mlem  13639  prdsgrpd  13650  prdsinvgd  13651  eqglact  13770  ghmgrp2  13791  ghmlin  13793  ghmnsgpreima  13814  kerf1ghm  13819  srgdilem  13940  srgdir  13946  srgridm  13951  ringdilem  13983  ringdir  13990  ringridm  13995  unitmulcl  14085  unitnegcl  14102  rhmmhm  14131  elrhmunit  14149  lringuplu  14168  subrgring  14196  subrg1cl  14201  qusrhm  14500  znunit  14631  znrrg  14632  psrelbas  14647  mplsubgfilemcl  14671  mplsubgfileminv  14672  inopn  14685  restbasg  14850  ssrest  14864  cntop2  14884  icnpimaex  14893  cnima  14902  lmfss  14926  lmtopcnp  14932  txhmeo  15001  txswaphmeo  15003  psmet0  15009  psmettri2  15010  blhalf  15090  bdxmet  15183  xmetxpbl  15190  ioo2bl  15233  tgioo  15236  cncfi  15260  rescncf  15263  cdivcncfap  15286  cnopnap  15293  divcncfap  15296  dedekindeulemeu  15304  dedekindicclemeu  15313  ivthinclemum  15317  ivthinclemlopn  15318  ivthinclemuopn  15320  ivthinclemdisj  15322  ivthdec  15326  ivthreinc  15327  limcimo  15347  cnplimcim  15349  cnplimclemr  15351  cnlimci  15355  limccnpcntop  15357  limccnp2lem  15358  limccnp2cntop  15359  limccoap  15360  reldvg  15361  dvbsssg  15368  dvfgg  15370  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvcjbr  15390  dvrecap  15395  plyco  15441  plycj  15443  plyrecj  15445  sin0pilem1  15463  sin0pilem2  15464  tanrpcl  15519  tangtx  15520  cos0pilt1  15534  logbgcd1irraplemexp  15650  mpodvdsmulf1o  15672  perfect  15683  lgsne0  15725  lgseisen  15761  lgsquad2lem2  15769  2sqlem8a  15809  2sqlem8  15810  structgrssiedg  15852  uhgrm  15886  umgredgne  15956  usgruspgrben  15992  usgredgppren  16003  umgr2edg  16013  wlkpropg  16045  wlkv  16047  wlkvtxeledgg  16065  g0wlk0  16091  trlsv  16103  bj-charfunbi  16198  bj-inf2vnlem1  16357  pwf1oexmid  16394  subctctexmid  16395  iooref1o  16432  taupi  16471  alsi2d  16480  alsc2d  16482