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  1000  simp3  1001  sbh  1787  eldifbd  3165  unssbd  3337  opth  4266  potr  4339  frind  4383  brrelex2  4700  funinsn  5303  feu  5436  fcnvres  5437  fun11iun  5521  elmpocl2  6115  uchoice  6190  oprssdmm  6224  tfrlem1  6361  tfrlemisucfn  6377  tfrlemisucaccv  6378  tfrlemibxssdm  6380  tfrlemibfn  6381  tfrlemi14d  6386  swoer  6615  elmapssres  6727  mapsspm  6736  pmsspw  6737  mapss  6745  dom0  6894  xpf1o  6900  sbthlemi8  7023  sbthlemi9  7024  supelti  7061  supisoti  7069  djulclb  7114  nninfninc  7182  nnnninfeq2  7188  cardcl  7241  isnumi  7242  cardval3ex  7245  exmidonfinlem  7253  en2eleq  7255  acfun  7267  exmidaclem  7268  dftap2  7311  exmidapne  7320  ccfunen  7324  indpi  7402  dfplpq2  7414  ltbtwnnq  7476  enq0tr  7494  nqnq0pi  7498  elnp1st2nd  7536  prcunqu  7545  prnmaxl  7548  prloc  7551  genpcuu  7580  addnqprllem  7587  addlocprlemeq  7593  addlocprlemgt  7594  addlocpr  7596  nqprxx  7606  gtnqex  7610  appdivnq  7623  prmuloclemcalc  7625  prmuloc  7626  mullocprlem  7630  ltprordil  7649  ltnqpri  7654  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  ltexpri  7673  recexprlemell  7682  recexprlemelu  7683  recexprlemloc  7691  recexprlempr  7692  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1l  7695  aptipr  7701  cauappcvgprlemlol  7707  cauappcvgprlemupu  7709  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdrl  7717  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemlol  7730  caucvgprlemupu  7732  caucvgprlemladdfu  7737  caucvgprlem1  7739  caucvgprlem2  7740  caucvgprprlemnjltk  7751  caucvgprprlemnbj  7753  caucvgprprlemlol  7758  caucvgprprlemupu  7760  caucvgprprlemexbt  7766  caucvgprprlem1  7769  caucvgprprlem2  7770  suplocexprlemrl  7777  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemub  7783  suplocexprlemlub  7784  ltsrprg  7807  gt0srpr  7808  recexgt0sr  7833  addgt0sr  7835  mulgt0sr  7838  map2psrprg  7865  suplocsrlemb  7866  suplocsrlem  7868  nnindnn  7953  axcaucvglemcau  7958  axpre-suploclemres  7961  apreap  8606  apreim  8622  mulge0  8638  apti  8641  mulap0bbd  8679  lble  8966  nnind  8998  recnz  9410  uzind  9428  eluzadd  9621  eluzsub  9622  ixxss1  9970  ixxss2  9971  ixxss12  9972  iccss2  10010  iccssioo2  10012  iccssico2  10013  elfzolt2  10223  ioom  10329  elicore  10335  flqltp1  10348  addmodlteq  10469  expcl2lemap  10622  expap0i  10642  hashennnuni  10850  wrdexb  10926  crre  11001  caucvgre  11125  cvg1nlemcau  11128  cvg1nlemres  11129  resqrexlemoverl  11165  sqrtge0  11177  fimaxre2  11370  climi  11430  reccn2ap  11456  climge0  11468  nnf1o  11519  sumpr  11556  fsump1i  11576  fsum00  11605  fsumparts  11613  mertenslemi1  11678  addsin  11885  subsin  11886  addcos  11889  subcos  11890  sinbnd2  11897  cosbnd2  11898  sinltxirr  11904  dvdsaddre2b  11984  evenelz  12008  4dvdseven  12058  infssuzcldc  12088  gcd0id  12116  gcd1  12124  bezoutlemstep  12134  dvdsgcdb  12150  mulgcd  12153  gcdzeq  12159  dvdsmulgcd  12162  sqgcd  12166  dvdssqlem  12167  bezoutr  12169  uzwodc  12174  nninfctlemfo  12177  lcmval  12201  lcmcllem  12205  lcmgcdlem  12215  lcmdvds  12217  lcmgcdeq  12221  lcmdvdsb  12222  mulgcddvds  12232  rpmulgcd2  12233  qredeu  12235  rpdvds  12237  divgcdcoprm0  12239  isprm3  12256  divgcdodd  12281  coprm  12282  rpexp  12291  sqrt2irr  12300  qdencl  12327  qeqnumdivden  12332  divnumden  12334  divdenle  12335  densq  12342  phimullem  12363  eulerthlem1  12365  eulerthlemrprm  12367  eulerthlemth  12370  prmdiveq  12374  prmdivdiv  12375  hashgcdeq  12377  phisum  12378  odzid  12382  reumodprminv  12391  oddn2prm  12399  pythagtriplem4  12406  pythagtriplem11  12412  pythagtriplem13  12414  pythagtriplem19  12420  pclemub  12425  pcprendvds2  12429  pcpre1  12430  pcpremul  12431  pceulem  12432  pczdvds  12452  pc2dvds  12468  pcaddlem  12477  pcmpt  12481  pcmpt2  12482  pcmptdvds  12483  pcprod  12484  pockthlem  12494  pockthg  12495  prmunb  12500  1arithlem4  12504  4sqlem7  12522  4sqlem8  12523  4sqlem9  12524  4sqlem10  12525  4sqlemffi  12534  4sqlem15  12543  4sqlem16  12544  4sqlem17  12545  4sqlem18  12546  ennnfonelemom  12565  ennnfonelemex  12571  ennnfonelemf1  12575  ctiunctlemu1st  12591  ctiunctlemu2nd  12592  fnpr2ob  12923  mgmlrid  12962  gsumfzval  12974  gsumval2  12980  mndrid  13017  grpinvcnv  13140  dfgrp3mlem  13170  eqglact  13295  ghmgrp2  13316  ghmlin  13318  ghmnsgpreima  13339  kerf1ghm  13344  srgdilem  13465  srgdir  13471  srgridm  13476  ringdilem  13508  ringdir  13515  ringridm  13520  unitmulcl  13609  unitnegcl  13626  rhmmhm  13655  elrhmunit  13673  lringuplu  13692  subrgring  13720  subrg1cl  13725  qusrhm  14024  znunit  14147  znrrg  14148  psrelbas  14160  inopn  14171  restbasg  14336  ssrest  14350  cntop2  14370  icnpimaex  14379  cnima  14388  lmfss  14412  lmtopcnp  14418  txhmeo  14487  txswaphmeo  14489  psmet0  14495  psmettri2  14496  blhalf  14576  bdxmet  14669  xmetxpbl  14676  ioo2bl  14711  tgioo  14714  cncfi  14733  rescncf  14736  cdivcncfap  14758  cnopnap  14765  divcncfap  14768  dedekindeulemeu  14776  dedekindicclemeu  14785  ivthinclemum  14789  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthinclemdisj  14794  ivthdec  14798  ivthreinc  14799  limcimo  14819  cnplimcim  14821  cnplimclemr  14823  cnlimci  14827  limccnpcntop  14829  limccnp2lem  14830  limccnp2cntop  14831  limccoap  14832  reldvg  14833  dvbsssg  14840  dvfgg  14842  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvrecap  14862  sin0pilem1  14916  sin0pilem2  14917  tanrpcl  14972  tangtx  14973  cos0pilt1  14987  logbgcd1irraplemexp  15100  lgsne0  15154  lgseisen  15190  2sqlem8a  15209  2sqlem8  15210  bj-charfunbi  15303  bj-inf2vnlem1  15462  pwf1oexmid  15490  subctctexmid  15491  iooref1o  15524  taupi  15563  alsi2d  15572  alsc2d  15574