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  1001  simp3  1002  sbh  1800  eldifbd  3179  unssbd  3352  opth  4285  potr  4359  frind  4403  brrelex2  4720  funinsn  5328  feu  5465  fcnvres  5466  fun11iun  5550  funopsn  5769  elmpocl2  6150  uchoice  6230  oprssdmm  6264  tfrlem1  6401  tfrlemisucfn  6417  tfrlemisucaccv  6418  tfrlemibxssdm  6420  tfrlemibfn  6421  tfrlemi14d  6426  swoer  6655  elmapssres  6767  mapsspm  6776  pmsspw  6777  mapss  6785  dom0  6942  xpf1o  6948  sbthlemi8  7073  sbthlemi9  7074  supelti  7111  supisoti  7119  djulclb  7164  nninfninc  7232  nnnninfeq2  7238  cardcl  7295  isnumi  7296  cardval3ex  7299  exmidonfinlem  7308  en2eleq  7310  finacn  7323  acfun  7326  exmidaclem  7327  dftap2  7370  exmidapne  7379  ccfunen  7383  acnccim  7391  indpi  7462  dfplpq2  7474  ltbtwnnq  7536  enq0tr  7554  nqnq0pi  7558  elnp1st2nd  7596  prcunqu  7605  prnmaxl  7608  prloc  7611  genpcuu  7640  addnqprllem  7647  addlocprlemeq  7653  addlocprlemgt  7654  addlocpr  7656  nqprxx  7666  gtnqex  7670  appdivnq  7683  prmuloclemcalc  7685  prmuloc  7686  mullocprlem  7690  ltprordil  7709  ltnqpri  7714  ltexprlemm  7720  ltexprlemopl  7721  ltexprlemlol  7722  ltexprlemopu  7723  ltexprlemupu  7724  ltexprlemdisj  7726  ltexprlemloc  7727  ltexprlemfl  7729  ltexprlemrl  7730  ltexprlemfu  7731  ltexprlemru  7732  ltexpri  7733  recexprlemell  7742  recexprlemelu  7743  recexprlemloc  7751  recexprlempr  7752  recexprlem1ssl  7753  recexprlem1ssu  7754  recexprlemss1l  7755  aptipr  7761  cauappcvgprlemlol  7767  cauappcvgprlemupu  7769  cauappcvgprlemladdfu  7774  cauappcvgprlemladdfl  7775  cauappcvgprlemladdrl  7777  caucvgprlemnkj  7786  caucvgprlemnbj  7787  caucvgprlemlol  7790  caucvgprlemupu  7792  caucvgprlemladdfu  7797  caucvgprlem1  7799  caucvgprlem2  7800  caucvgprprlemnjltk  7811  caucvgprprlemnbj  7813  caucvgprprlemlol  7818  caucvgprprlemupu  7820  caucvgprprlemexbt  7826  caucvgprprlem1  7829  caucvgprprlem2  7830  suplocexprlemrl  7837  suplocexprlemru  7839  suplocexprlemdisj  7840  suplocexprlemub  7843  suplocexprlemlub  7844  ltsrprg  7867  gt0srpr  7868  recexgt0sr  7893  addgt0sr  7895  mulgt0sr  7898  map2psrprg  7925  suplocsrlemb  7926  suplocsrlem  7928  nnindnn  8013  axcaucvglemcau  8018  axpre-suploclemres  8021  apreap  8667  apreim  8683  mulge0  8699  apti  8702  mulap0bbd  8740  lble  9027  nnind  9059  recnz  9473  uzind  9491  eluzadd  9684  eluzsub  9685  ixxss1  10033  ixxss2  10034  ixxss12  10035  iccss2  10073  iccssioo2  10075  iccssico2  10076  elfzolt2  10286  infssuzcldc  10385  ioom  10410  elicore  10416  flqltp1  10429  addmodlteq  10550  expcl2lemap  10703  expap0i  10723  hashennnuni  10931  hashdmprop2dom  10996  wrdexb  11013  swrdsbslen  11127  swrdspsleq  11128  crre  11212  caucvgre  11336  cvg1nlemcau  11339  cvg1nlemres  11340  resqrexlemoverl  11376  sqrtge0  11388  fimaxre2  11582  climi  11642  reccn2ap  11668  climge0  11680  nnf1o  11731  sumpr  11768  fsump1i  11788  fsum00  11817  fsumparts  11825  mertenslemi1  11890  addsin  12097  subsin  12098  addcos  12101  subcos  12102  sinbnd2  12109  cosbnd2  12110  sinltxirr  12116  dvdsaddre2b  12196  evenelz  12222  4dvdseven  12272  gcd0id  12344  gcd1  12352  bezoutlemstep  12362  dvdsgcdb  12378  mulgcd  12381  gcdzeq  12387  dvdsmulgcd  12390  sqgcd  12394  dvdssqlem  12395  bezoutr  12397  uzwodc  12402  nninfctlemfo  12405  lcmval  12429  lcmcllem  12433  lcmgcdlem  12443  lcmdvds  12445  lcmgcdeq  12449  lcmdvdsb  12450  mulgcddvds  12460  rpmulgcd2  12461  qredeu  12463  rpdvds  12465  divgcdcoprm0  12467  isprm3  12484  divgcdodd  12509  coprm  12510  rpexp  12519  sqrt2irr  12528  qdencl  12555  qeqnumdivden  12560  divnumden  12562  divdenle  12563  densq  12570  phimullem  12591  eulerthlem1  12593  eulerthlemrprm  12595  eulerthlemth  12598  prmdiveq  12602  prmdivdiv  12603  hashgcdeq  12606  phisum  12607  odzid  12611  reumodprminv  12620  oddn2prm  12628  pythagtriplem4  12635  pythagtriplem11  12641  pythagtriplem13  12643  pythagtriplem19  12649  pclemub  12654  pcprendvds2  12658  pcpre1  12659  pcpremul  12660  pceulem  12661  pczdvds  12681  pc2dvds  12697  pcaddlem  12706  pcmpt  12710  pcmpt2  12711  pcmptdvds  12712  pcprod  12713  pockthlem  12723  pockthg  12724  prmunb  12729  1arithlem4  12733  4sqlem7  12751  4sqlem8  12752  4sqlem9  12753  4sqlem10  12754  4sqlemffi  12763  4sqlem15  12772  4sqlem16  12773  4sqlem17  12774  4sqlem18  12775  ennnfonelemom  12823  ennnfonelemex  12829  ennnfonelemf1  12833  ctiunctlemu1st  12849  ctiunctlemu2nd  12850  fnpr2ob  13216  mgmlrid  13255  gsumfzval  13267  gsumval2  13273  mndrid  13312  prdsmndd  13324  grpinvcnv  13444  dfgrp3mlem  13474  prdsgrpd  13485  prdsinvgd  13486  eqglact  13605  ghmgrp2  13626  ghmlin  13628  ghmnsgpreima  13649  kerf1ghm  13654  srgdilem  13775  srgdir  13781  srgridm  13786  ringdilem  13818  ringdir  13825  ringridm  13830  unitmulcl  13919  unitnegcl  13936  rhmmhm  13965  elrhmunit  13983  lringuplu  14002  subrgring  14030  subrg1cl  14035  qusrhm  14334  znunit  14465  znrrg  14466  psrelbas  14481  mplsubgfilemcl  14505  mplsubgfileminv  14506  inopn  14519  restbasg  14684  ssrest  14698  cntop2  14718  icnpimaex  14727  cnima  14736  lmfss  14760  lmtopcnp  14766  txhmeo  14835  txswaphmeo  14837  psmet0  14843  psmettri2  14844  blhalf  14924  bdxmet  15017  xmetxpbl  15024  ioo2bl  15067  tgioo  15070  cncfi  15094  rescncf  15097  cdivcncfap  15120  cnopnap  15127  divcncfap  15130  dedekindeulemeu  15138  dedekindicclemeu  15147  ivthinclemum  15151  ivthinclemlopn  15152  ivthinclemuopn  15154  ivthinclemdisj  15156  ivthdec  15160  ivthreinc  15161  limcimo  15181  cnplimcim  15183  cnplimclemr  15185  cnlimci  15189  limccnpcntop  15191  limccnp2lem  15192  limccnp2cntop  15193  limccoap  15194  reldvg  15195  dvbsssg  15202  dvfgg  15204  dvaddxxbr  15217  dvmulxxbr  15218  dvcoapbr  15223  dvcjbr  15224  dvrecap  15229  plyco  15275  plycj  15277  plyrecj  15279  sin0pilem1  15297  sin0pilem2  15298  tanrpcl  15353  tangtx  15354  cos0pilt1  15368  logbgcd1irraplemexp  15484  mpodvdsmulf1o  15506  perfect  15517  lgsne0  15559  lgseisen  15595  lgsquad2lem2  15603  2sqlem8a  15643  2sqlem8  15644  structgrssiedg  15686  uhgrm  15718  bj-charfunbi  15821  bj-inf2vnlem1  15980  pwf1oexmid  16010  subctctexmid  16011  iooref1o  16047  taupi  16086  alsi2d  16095  alsc2d  16097