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  simplrd  530  simprld  532  simprrd  534  simp2  1024  simp3  1025  sbh  1824  eldifbd  3212  unssbd  3385  opth  4329  potr  4405  frind  4449  brrelex2  4767  funinsn  5379  feu  5519  fcnvres  5520  fun11iun  5604  funopsn  5830  elmpocl2  6219  uchoice  6300  oprssdmm  6334  tfrlem1  6474  tfrlemisucfn  6490  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemi14d  6499  swoer  6730  elmapssres  6842  mapsspm  6851  pmsspw  6852  mapss  6860  dom0  7024  xpf1o  7030  sbthlemi8  7163  sbthlemi9  7164  supelti  7201  supisoti  7209  djulclb  7254  nninfninc  7322  nnnninfeq2  7328  cardcl  7385  isnumi  7386  cardval3ex  7389  exmidonfinlem  7404  en2eleq  7406  finacn  7419  acfun  7422  exmidaclem  7423  pw1if  7443  dftap2  7470  exmidapne  7479  ccfunen  7483  acnccim  7491  indpi  7562  dfplpq2  7574  ltbtwnnq  7636  enq0tr  7654  nqnq0pi  7658  elnp1st2nd  7696  prcunqu  7705  prnmaxl  7708  prloc  7711  genpcuu  7740  addnqprllem  7747  addlocprlemeq  7753  addlocprlemgt  7754  addlocpr  7756  nqprxx  7766  gtnqex  7770  appdivnq  7783  prmuloclemcalc  7785  prmuloc  7786  mullocprlem  7790  ltprordil  7809  ltnqpri  7814  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  ltexpri  7833  recexprlemell  7842  recexprlemelu  7843  recexprlemloc  7851  recexprlempr  7852  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  aptipr  7861  cauappcvgprlemlol  7867  cauappcvgprlemupu  7869  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdrl  7877  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemlol  7890  caucvgprlemupu  7892  caucvgprlemladdfu  7897  caucvgprlem1  7899  caucvgprlem2  7900  caucvgprprlemnjltk  7911  caucvgprprlemnbj  7913  caucvgprprlemlol  7918  caucvgprprlemupu  7920  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  suplocexprlemrl  7937  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemub  7943  suplocexprlemlub  7944  ltsrprg  7967  gt0srpr  7968  recexgt0sr  7993  addgt0sr  7995  mulgt0sr  7998  map2psrprg  8025  suplocsrlemb  8026  suplocsrlem  8028  nnindnn  8113  axcaucvglemcau  8118  axpre-suploclemres  8121  apreap  8767  apreim  8783  mulge0  8799  apti  8802  mulap0bbd  8840  lble  9127  nnind  9159  recnz  9573  uzind  9591  eluzadd  9785  eluzsub  9786  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  iccssioo2  10181  iccssico2  10182  elfzolt2  10392  infssuzcldc  10496  ioom  10521  elicore  10527  flqltp1  10540  addmodlteq  10661  expcl2lemap  10814  expap0i  10834  hashennnuni  11042  hashdmprop2dom  11109  wrdexb  11126  swrdsbslen  11248  swrdspsleq  11249  crre  11419  caucvgre  11543  cvg1nlemcau  11546  cvg1nlemres  11547  resqrexlemoverl  11583  sqrtge0  11595  fimaxre2  11789  climi  11849  reccn2ap  11875  climge0  11887  nnf1o  11939  sumpr  11976  fsump1i  11996  fsum00  12025  fsumparts  12033  mertenslemi1  12098  addsin  12305  subsin  12306  addcos  12309  subcos  12310  sinbnd2  12317  cosbnd2  12318  sinltxirr  12324  dvdsaddre2b  12404  evenelz  12430  4dvdseven  12480  gcd0id  12552  gcd1  12560  bezoutlemstep  12570  dvdsgcdb  12586  mulgcd  12589  gcdzeq  12595  dvdsmulgcd  12598  sqgcd  12602  dvdssqlem  12603  bezoutr  12605  uzwodc  12610  nninfctlemfo  12613  lcmval  12637  lcmcllem  12641  lcmgcdlem  12651  lcmdvds  12653  lcmgcdeq  12657  lcmdvdsb  12658  mulgcddvds  12668  rpmulgcd2  12669  qredeu  12671  rpdvds  12673  divgcdcoprm0  12675  isprm3  12692  divgcdodd  12717  coprm  12718  rpexp  12727  sqrt2irr  12736  qdencl  12763  qeqnumdivden  12768  divnumden  12770  divdenle  12771  densq  12778  phimullem  12799  eulerthlem1  12801  eulerthlemrprm  12803  eulerthlemth  12806  prmdiveq  12810  prmdivdiv  12811  hashgcdeq  12814  phisum  12815  odzid  12819  reumodprminv  12828  oddn2prm  12836  pythagtriplem4  12843  pythagtriplem11  12849  pythagtriplem13  12851  pythagtriplem19  12857  pclemub  12862  pcprendvds2  12866  pcpre1  12867  pcpremul  12868  pceulem  12869  pczdvds  12889  pc2dvds  12905  pcaddlem  12914  pcmpt  12918  pcmpt2  12919  pcmptdvds  12920  pcprod  12921  pockthlem  12931  pockthg  12932  prmunb  12937  1arithlem4  12941  4sqlem7  12959  4sqlem8  12960  4sqlem9  12961  4sqlem10  12962  4sqlemffi  12971  4sqlem15  12980  4sqlem16  12981  4sqlem17  12982  4sqlem18  12983  ennnfonelemom  13031  ennnfonelemex  13037  ennnfonelemf1  13041  ctiunctlemu1st  13057  ctiunctlemu2nd  13058  fnpr2ob  13425  mgmlrid  13464  gsumfzval  13476  gsumval2  13482  mndrid  13521  prdsmndd  13533  grpinvcnv  13653  dfgrp3mlem  13683  prdsgrpd  13694  prdsinvgd  13695  eqglact  13814  ghmgrp2  13835  ghmlin  13837  ghmnsgpreima  13858  kerf1ghm  13863  gsumsplit0  13935  srgdilem  13985  srgdir  13991  srgridm  13996  ringdilem  14028  ringdir  14035  ringridm  14040  unitmulcl  14130  unitnegcl  14147  rhmmhm  14176  elrhmunit  14194  lringuplu  14213  subrgring  14241  subrg1cl  14246  qusrhm  14545  znunit  14676  znrrg  14677  psrelbas  14692  mplsubgfilemcl  14716  mplsubgfileminv  14717  inopn  14730  restbasg  14895  ssrest  14909  cntop2  14929  icnpimaex  14938  cnima  14947  lmfss  14971  lmtopcnp  14977  txhmeo  15046  txswaphmeo  15048  psmet0  15054  psmettri2  15055  blhalf  15135  bdxmet  15228  xmetxpbl  15235  ioo2bl  15278  tgioo  15281  cncfi  15305  rescncf  15308  cdivcncfap  15331  cnopnap  15338  divcncfap  15341  dedekindeulemeu  15349  dedekindicclemeu  15358  ivthinclemum  15362  ivthinclemlopn  15363  ivthinclemuopn  15365  ivthinclemdisj  15367  ivthdec  15371  ivthreinc  15372  limcimo  15392  cnplimcim  15394  cnplimclemr  15396  cnlimci  15400  limccnpcntop  15402  limccnp2lem  15403  limccnp2cntop  15404  limccoap  15405  reldvg  15406  dvbsssg  15413  dvfgg  15415  dvaddxxbr  15428  dvmulxxbr  15429  dvcoapbr  15434  dvcjbr  15435  dvrecap  15440  plyco  15486  plycj  15488  plyrecj  15490  sin0pilem1  15508  sin0pilem2  15509  tanrpcl  15564  tangtx  15565  cos0pilt1  15579  logbgcd1irraplemexp  15695  mpodvdsmulf1o  15717  perfect  15728  lgsne0  15770  lgseisen  15806  lgsquad2lem2  15814  2sqlem8a  15854  2sqlem8  15855  structgrssiedg  15897  uhgrm  15932  umgredgne  16004  usgruspgrben  16040  usgredgppren  16051  umgr2edg  16061  vtxdumgrfival  16152  wlkpropg  16178  wlkv  16180  wlkvtxeledgg  16198  g0wlk0  16224  trlsv  16238  clwwlknlen  16265  eupthv  16300  eupthf1o  16304  eupth2lem3lem4fi  16327  bj-charfunbi  16427  bj-inf2vnlem1  16586  pwf1oexmid  16621  subctctexmid  16622  iooref1o  16659  taupi  16698  alsi2d  16717  alsc2d  16719