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  1823  eldifbd  3211  unssbd  3384  opth  4331  potr  4407  frind  4451  brrelex2  4769  funinsn  5381  feu  5521  fcnvres  5522  fun11iun  5607  funopsn  5833  elmpocl2  6224  uchoice  6305  oprssdmm  6339  tfrlem1  6479  tfrlemisucfn  6495  tfrlemisucaccv  6496  tfrlemibxssdm  6498  tfrlemibfn  6499  tfrlemi14d  6504  swoer  6735  elmapssres  6847  mapsspm  6856  pmsspw  6857  mapss  6865  dom0  7029  xpf1o  7035  sbthlemi8  7168  sbthlemi9  7169  supelti  7206  supisoti  7214  djulclb  7259  nninfninc  7327  nnnninfeq2  7333  cardcl  7390  isnumi  7391  cardval3ex  7394  exmidonfinlem  7409  en2eleq  7411  finacn  7424  acfun  7427  exmidaclem  7428  pw1if  7448  dftap2  7475  exmidapne  7484  ccfunen  7488  acnccim  7496  indpi  7567  dfplpq2  7579  ltbtwnnq  7641  enq0tr  7659  nqnq0pi  7663  elnp1st2nd  7701  prcunqu  7710  prnmaxl  7713  prloc  7716  genpcuu  7745  addnqprllem  7752  addlocprlemeq  7758  addlocprlemgt  7759  addlocpr  7761  nqprxx  7771  gtnqex  7775  appdivnq  7788  prmuloclemcalc  7790  prmuloc  7791  mullocprlem  7795  ltprordil  7814  ltnqpri  7819  ltexprlemm  7825  ltexprlemopl  7826  ltexprlemlol  7827  ltexprlemopu  7828  ltexprlemupu  7829  ltexprlemdisj  7831  ltexprlemloc  7832  ltexprlemfl  7834  ltexprlemrl  7835  ltexprlemfu  7836  ltexprlemru  7837  ltexpri  7838  recexprlemell  7847  recexprlemelu  7848  recexprlemloc  7856  recexprlempr  7857  recexprlem1ssl  7858  recexprlem1ssu  7859  recexprlemss1l  7860  aptipr  7866  cauappcvgprlemlol  7872  cauappcvgprlemupu  7874  cauappcvgprlemladdfu  7879  cauappcvgprlemladdfl  7880  cauappcvgprlemladdrl  7882  caucvgprlemnkj  7891  caucvgprlemnbj  7892  caucvgprlemlol  7895  caucvgprlemupu  7897  caucvgprlemladdfu  7902  caucvgprlem1  7904  caucvgprlem2  7905  caucvgprprlemnjltk  7916  caucvgprprlemnbj  7918  caucvgprprlemlol  7923  caucvgprprlemupu  7925  caucvgprprlemexbt  7931  caucvgprprlem1  7934  caucvgprprlem2  7935  suplocexprlemrl  7942  suplocexprlemru  7944  suplocexprlemdisj  7945  suplocexprlemub  7948  suplocexprlemlub  7949  ltsrprg  7972  gt0srpr  7973  recexgt0sr  7998  addgt0sr  8000  mulgt0sr  8003  map2psrprg  8030  suplocsrlemb  8031  suplocsrlem  8033  nnindnn  8118  axcaucvglemcau  8123  axpre-suploclemres  8126  apreap  8772  apreim  8788  mulge0  8804  apti  8807  mulap0bbd  8845  lble  9132  nnind  9164  recnz  9578  uzind  9596  eluzadd  9790  eluzsub  9791  ixxss1  10144  ixxss2  10145  ixxss12  10146  iccss2  10184  iccssioo2  10186  iccssico2  10187  elfzolt2  10397  infssuzcldc  10501  ioom  10526  elicore  10532  flqltp1  10545  addmodlteq  10666  expcl2lemap  10819  expap0i  10839  hashennnuni  11047  hashdmprop2dom  11114  wrdexb  11134  swrdsbslen  11256  swrdspsleq  11257  crre  11440  caucvgre  11564  cvg1nlemcau  11567  cvg1nlemres  11568  resqrexlemoverl  11604  sqrtge0  11616  fimaxre2  11810  climi  11870  reccn2ap  11896  climge0  11908  nnf1o  11960  sumpr  11997  fsump1i  12017  fsum00  12046  fsumparts  12054  mertenslemi1  12119  addsin  12326  subsin  12327  addcos  12330  subcos  12331  sinbnd2  12338  cosbnd2  12339  sinltxirr  12345  dvdsaddre2b  12425  evenelz  12451  4dvdseven  12501  gcd0id  12573  gcd1  12581  bezoutlemstep  12591  dvdsgcdb  12607  mulgcd  12610  gcdzeq  12616  dvdsmulgcd  12619  sqgcd  12623  dvdssqlem  12624  bezoutr  12626  uzwodc  12631  nninfctlemfo  12634  lcmval  12658  lcmcllem  12662  lcmgcdlem  12672  lcmdvds  12674  lcmgcdeq  12678  lcmdvdsb  12679  mulgcddvds  12689  rpmulgcd2  12690  qredeu  12692  rpdvds  12694  divgcdcoprm0  12696  isprm3  12713  divgcdodd  12738  coprm  12739  rpexp  12748  sqrt2irr  12757  qdencl  12784  qeqnumdivden  12789  divnumden  12791  divdenle  12792  densq  12799  phimullem  12820  eulerthlem1  12822  eulerthlemrprm  12824  eulerthlemth  12827  prmdiveq  12831  prmdivdiv  12832  hashgcdeq  12835  phisum  12836  odzid  12840  reumodprminv  12849  oddn2prm  12857  pythagtriplem4  12864  pythagtriplem11  12870  pythagtriplem13  12872  pythagtriplem19  12878  pclemub  12883  pcprendvds2  12887  pcpre1  12888  pcpremul  12889  pceulem  12890  pczdvds  12910  pc2dvds  12926  pcaddlem  12935  pcmpt  12939  pcmpt2  12940  pcmptdvds  12941  pcprod  12942  pockthlem  12952  pockthg  12953  prmunb  12958  1arithlem4  12962  4sqlem7  12980  4sqlem8  12981  4sqlem9  12982  4sqlem10  12983  4sqlemffi  12992  4sqlem15  13001  4sqlem16  13002  4sqlem17  13003  4sqlem18  13004  ennnfonelemom  13052  ennnfonelemex  13058  ennnfonelemf1  13062  ctiunctlemu1st  13078  ctiunctlemu2nd  13079  fnpr2ob  13446  mgmlrid  13485  gsumfzval  13497  gsumval2  13503  mndrid  13542  prdsmndd  13554  grpinvcnv  13674  dfgrp3mlem  13704  prdsgrpd  13715  prdsinvgd  13716  eqglact  13835  ghmgrp2  13856  ghmlin  13858  ghmnsgpreima  13879  kerf1ghm  13884  gsumsplit0  13956  srgdilem  14006  srgdir  14012  srgridm  14017  ringdilem  14049  ringdir  14056  ringridm  14061  unitmulcl  14151  unitnegcl  14168  rhmmhm  14197  elrhmunit  14215  lringuplu  14234  subrgring  14262  subrg1cl  14267  qusrhm  14566  znunit  14697  znrrg  14698  psrbaglecl  14713  psrbagcon  14714  psrbagconcl  14715  psrelbas  14718  mplsubgfilemcl  14742  mplsubgfileminv  14743  inopn  14756  restbasg  14921  ssrest  14935  cntop2  14955  icnpimaex  14964  cnima  14973  lmfss  14997  lmtopcnp  15003  txhmeo  15072  txswaphmeo  15074  psmet0  15080  psmettri2  15081  blhalf  15161  bdxmet  15254  xmetxpbl  15261  ioo2bl  15304  tgioo  15307  cncfi  15331  rescncf  15334  cdivcncfap  15357  cnopnap  15364  divcncfap  15367  dedekindeulemeu  15375  dedekindicclemeu  15384  ivthinclemum  15388  ivthinclemlopn  15389  ivthinclemuopn  15391  ivthinclemdisj  15393  ivthdec  15397  ivthreinc  15398  limcimo  15418  cnplimcim  15420  cnplimclemr  15422  cnlimci  15426  limccnpcntop  15428  limccnp2lem  15429  limccnp2cntop  15430  limccoap  15431  reldvg  15432  dvbsssg  15439  dvfgg  15441  dvaddxxbr  15454  dvmulxxbr  15455  dvcoapbr  15460  dvcjbr  15461  dvrecap  15466  plyco  15512  plycj  15514  plyrecj  15516  sin0pilem1  15534  sin0pilem2  15535  tanrpcl  15590  tangtx  15591  cos0pilt1  15605  logbgcd1irraplemexp  15721  mpodvdsmulf1o  15743  perfect  15754  lgsne0  15796  lgseisen  15832  lgsquad2lem2  15840  2sqlem8a  15880  2sqlem8  15881  structgrssiedg  15923  uhgrm  15958  umgredgne  16030  usgruspgrben  16066  usgredgppren  16077  umgr2edg  16087  vtxdumgrfival  16178  wlkpropg  16204  wlkv  16206  wlkvtxeledgg  16224  g0wlk0  16250  trlsv  16264  clwwlknlen  16291  eupthv  16326  eupthf1o  16330  eupth2lem3lem4fi  16353  eulerpathprum  16360  bj-charfunbi  16466  bj-inf2vnlem1  16625  pwf1oexmid  16660  subctctexmid  16661  iooref1o  16705  taupi  16745  alsi2d  16764  alsc2d  16766