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  1025  simp3  1026  sbh  1825  eldifbd  3222  unssbd  3396  opth  4352  potr  4428  frind  4472  brrelex2  4790  funinsn  5404  feu  5548  fcnvres  5549  fun11iun  5634  funopsn  5859  elmpocl2  6250  uchoice  6330  oprssdmm  6364  fczsupp0  6458  tfrlem1  6538  tfrlemisucfn  6554  tfrlemisucaccv  6555  tfrlemibxssdm  6557  tfrlemibfn  6558  tfrlemi14d  6563  swoer  6794  elmapssres  6906  mapsspm  6915  pmsspw  6916  mapss  6925  dom0  7090  xpf1o  7096  sbthlemi8  7233  sbthlemi9  7234  fsuppimpd  7245  supelti  7292  supisoti  7300  djulclb  7345  nninfninc  7413  nnnninfeq2  7419  cardcl  7476  isnumi  7477  cardval3ex  7480  exmidonfinlem  7495  en2eleq  7497  finacn  7510  acfun  7513  exmidaclem  7514  pw1if  7534  dftap2  7561  exmidapne  7570  ccfunen  7574  acnccim  7582  indpi  7653  dfplpq2  7665  ltbtwnnq  7727  enq0tr  7745  nqnq0pi  7749  elnp1st2nd  7787  prcunqu  7796  prnmaxl  7799  prloc  7802  genpcuu  7831  addnqprllem  7838  addlocprlemeq  7844  addlocprlemgt  7845  addlocpr  7847  nqprxx  7857  gtnqex  7861  appdivnq  7874  prmuloclemcalc  7876  prmuloc  7877  mullocprlem  7881  ltprordil  7900  ltnqpri  7905  ltexprlemm  7911  ltexprlemopl  7912  ltexprlemlol  7913  ltexprlemopu  7914  ltexprlemupu  7915  ltexprlemdisj  7917  ltexprlemloc  7918  ltexprlemfl  7920  ltexprlemrl  7921  ltexprlemfu  7922  ltexprlemru  7923  ltexpri  7924  recexprlemell  7933  recexprlemelu  7934  recexprlemloc  7942  recexprlempr  7943  recexprlem1ssl  7944  recexprlem1ssu  7945  recexprlemss1l  7946  aptipr  7952  cauappcvgprlemlol  7958  cauappcvgprlemupu  7960  cauappcvgprlemladdfu  7965  cauappcvgprlemladdfl  7966  cauappcvgprlemladdrl  7968  caucvgprlemnkj  7977  caucvgprlemnbj  7978  caucvgprlemlol  7981  caucvgprlemupu  7983  caucvgprlemladdfu  7988  caucvgprlem1  7990  caucvgprlem2  7991  caucvgprprlemnjltk  8002  caucvgprprlemnbj  8004  caucvgprprlemlol  8009  caucvgprprlemupu  8011  caucvgprprlemexbt  8017  caucvgprprlem1  8020  caucvgprprlem2  8021  suplocexprlemrl  8028  suplocexprlemru  8030  suplocexprlemdisj  8031  suplocexprlemub  8034  suplocexprlemlub  8035  ltsrprg  8058  gt0srpr  8059  recexgt0sr  8084  addgt0sr  8086  mulgt0sr  8089  map2psrprg  8116  suplocsrlemb  8117  suplocsrlem  8119  nnindnn  8204  axcaucvglemcau  8209  axpre-suploclemres  8212  apreap  8857  apreim  8873  mulge0  8889  apti  8892  mulap0bbd  8930  lble  9217  nnind  9249  recnz  9667  uzind  9685  eluzadd  9879  eluzsub  9880  ixxss1  10233  ixxss2  10234  ixxss12  10235  iccss2  10273  iccssioo2  10275  iccssico2  10276  elfzolt2  10487  infssuzcldc  10591  ioom  10616  elicore  10622  flqltp1  10635  addmodlteq  10756  expcl2lemap  10909  expap0i  10929  hashennnuni  11137  hashdmprop2dom  11209  wrdexb  11229  swrdsbslen  11351  swrdspsleq  11352  crre  11535  caucvgre  11659  cvg1nlemcau  11662  cvg1nlemres  11663  resqrexlemoverl  11699  sqrtge0  11711  fimaxre2  11905  climi  11965  reccn2ap  11991  climge0  12003  nnf1o  12055  sumpr  12092  fsump1i  12112  fsum00  12141  fsumparts  12149  mertenslemi1  12214  addsin  12421  subsin  12422  addcos  12425  subcos  12426  sinbnd2  12433  cosbnd2  12434  sinltxirr  12440  dvdsaddre2b  12520  evenelz  12546  4dvdseven  12596  gcd0id  12668  gcd1  12676  bezoutlemstep  12686  dvdsgcdb  12702  mulgcd  12705  gcdzeq  12711  dvdsmulgcd  12714  sqgcd  12718  dvdssqlem  12719  bezoutr  12721  uzwodc  12726  nninfctlemfo  12729  lcmval  12753  lcmcllem  12757  lcmgcdlem  12767  lcmdvds  12769  lcmgcdeq  12773  lcmdvdsb  12774  mulgcddvds  12784  rpmulgcd2  12785  qredeu  12787  rpdvds  12789  divgcdcoprm0  12791  isprm3  12808  divgcdodd  12833  coprm  12834  rpexp  12843  sqrt2irr  12852  qdencl  12879  qeqnumdivden  12884  divnumden  12886  divdenle  12887  densq  12894  phimullem  12915  eulerthlem1  12917  eulerthlemrprm  12919  eulerthlemth  12922  prmdiveq  12926  prmdivdiv  12927  hashgcdeq  12930  phisum  12931  odzid  12935  reumodprminv  12944  oddn2prm  12952  pythagtriplem4  12959  pythagtriplem11  12965  pythagtriplem13  12967  pythagtriplem19  12973  pclemub  12978  pcprendvds2  12982  pcpre1  12983  pcpremul  12984  pceulem  12985  pczdvds  13005  pc2dvds  13021  pcaddlem  13030  pcmpt  13034  pcmpt2  13035  pcmptdvds  13036  pcprod  13037  pockthlem  13047  pockthg  13048  prmunb  13053  1arithlem4  13057  4sqlem7  13075  4sqlem8  13076  4sqlem9  13077  4sqlem10  13078  4sqlemffi  13087  4sqlem15  13096  4sqlem16  13097  4sqlem17  13098  4sqlem18  13099  ennnfonelemom  13148  ennnfonelemex  13154  ennnfonelemf1  13158  ctiunctlemu1st  13174  ctiunctlemu2nd  13175  fnpr2ob  13542  mgmlrid  13581  gsumfzval  13593  gsumval2  13599  mndrid  13638  prdsmndd  13650  grpinvcnv  13770  dfgrp3mlem  13800  prdsgrpd  13811  prdsinvgd  13812  eqglact  13931  ghmgrp2  13952  ghmlin  13954  ghmnsgpreima  13975  kerf1ghm  13980  gsumsplit0  14052  srgdilem  14102  srgdir  14108  srgridm  14113  ringdilem  14145  ringdir  14152  ringridm  14157  unitmulcl  14247  unitnegcl  14264  rhmmhm  14293  elrhmunit  14311  lringuplu  14330  subrgring  14358  subrg1cl  14363  qusrhm  14663  znunit  14794  znrrg  14795  psrbagfsupp  14806  psrbaglecl  14811  psrbagcon  14813  psrbagconcl  14814  psrelbas  14817  mplsubgfilemcl  14841  mplsubgfileminv  14842  inopn  14855  restbasg  15020  ssrest  15034  cntop2  15054  icnpimaex  15063  cnima  15072  lmfss  15096  lmtopcnp  15102  txhmeo  15171  txswaphmeo  15173  psmet0  15179  psmettri2  15180  blhalf  15260  bdxmet  15353  xmetxpbl  15360  ioo2bl  15403  tgioo  15406  cncfi  15430  rescncf  15433  cdivcncfap  15456  cnopnap  15463  divcncfap  15466  dedekindeulemeu  15474  dedekindicclemeu  15483  ivthinclemum  15487  ivthinclemlopn  15488  ivthinclemuopn  15490  ivthinclemdisj  15492  ivthdec  15496  ivthreinc  15497  limcimo  15517  cnplimcim  15519  cnplimclemr  15521  cnlimci  15525  limccnpcntop  15527  limccnp2lem  15528  limccnp2cntop  15529  limccoap  15530  reldvg  15531  dvbsssg  15538  dvfgg  15540  dvaddxxbr  15553  dvmulxxbr  15554  dvcoapbr  15559  dvcjbr  15560  dvrecap  15565  plyco  15611  plycj  15613  plyrecj  15615  sin0pilem1  15633  sin0pilem2  15634  tanrpcl  15689  tangtx  15690  cos0pilt1  15704  logbgcd1irraplemexp  15820  mpodvdsmulf1o  15845  perfect  15856  lgsne0  15898  lgseisen  15934  lgsquad2lem2  15942  2sqlem8a  15982  2sqlem8  15983  structgrssiedg  16025  uhgrm  16060  umgredgne  16132  usgruspgrben  16168  usgredgppren  16179  umgr2edg  16189  vtxdumgrfival  16280  wlkpropg  16306  wlkv  16308  wlkvtxeledgg  16326  g0wlk0  16352  trlsv  16366  clwwlknlen  16393  eupthv  16428  eupthf1o  16432  eupth2lem3lem4fi  16455  eulerpathprum  16462  bj-charfunbi  16568  bj-inf2vnlem1  16727  pwf1oexmid  16760  subctctexmid  16761  iooref1o  16805  taupi  16845  alsi2d  16865  alsc2d  16867