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  1790  eldifbd  3169  unssbd  3342  opth  4271  potr  4344  frind  4388  brrelex2  4705  funinsn  5308  feu  5443  fcnvres  5444  fun11iun  5528  elmpocl2  6124  uchoice  6204  oprssdmm  6238  tfrlem1  6375  tfrlemisucfn  6391  tfrlemisucaccv  6392  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemi14d  6400  swoer  6629  elmapssres  6741  mapsspm  6750  pmsspw  6751  mapss  6759  dom0  6908  xpf1o  6914  sbthlemi8  7039  sbthlemi9  7040  supelti  7077  supisoti  7085  djulclb  7130  nninfninc  7198  nnnninfeq2  7204  cardcl  7259  isnumi  7260  cardval3ex  7263  exmidonfinlem  7272  en2eleq  7274  finacn  7287  acfun  7290  exmidaclem  7291  dftap2  7334  exmidapne  7343  ccfunen  7347  acnccim  7355  indpi  7426  dfplpq2  7438  ltbtwnnq  7500  enq0tr  7518  nqnq0pi  7522  elnp1st2nd  7560  prcunqu  7569  prnmaxl  7572  prloc  7575  genpcuu  7604  addnqprllem  7611  addlocprlemeq  7617  addlocprlemgt  7618  addlocpr  7620  nqprxx  7630  gtnqex  7634  appdivnq  7647  prmuloclemcalc  7649  prmuloc  7650  mullocprlem  7654  ltprordil  7673  ltnqpri  7678  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemlol  7686  ltexprlemopu  7687  ltexprlemupu  7688  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemfl  7693  ltexprlemrl  7694  ltexprlemfu  7695  ltexprlemru  7696  ltexpri  7697  recexprlemell  7706  recexprlemelu  7707  recexprlemloc  7715  recexprlempr  7716  recexprlem1ssl  7717  recexprlem1ssu  7718  recexprlemss1l  7719  aptipr  7725  cauappcvgprlemlol  7731  cauappcvgprlemupu  7733  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdrl  7741  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemlol  7754  caucvgprlemupu  7756  caucvgprlemladdfu  7761  caucvgprlem1  7763  caucvgprlem2  7764  caucvgprprlemnjltk  7775  caucvgprprlemnbj  7777  caucvgprprlemlol  7782  caucvgprprlemupu  7784  caucvgprprlemexbt  7790  caucvgprprlem1  7793  caucvgprprlem2  7794  suplocexprlemrl  7801  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemub  7807  suplocexprlemlub  7808  ltsrprg  7831  gt0srpr  7832  recexgt0sr  7857  addgt0sr  7859  mulgt0sr  7862  map2psrprg  7889  suplocsrlemb  7890  suplocsrlem  7892  nnindnn  7977  axcaucvglemcau  7982  axpre-suploclemres  7985  apreap  8631  apreim  8647  mulge0  8663  apti  8666  mulap0bbd  8704  lble  8991  nnind  9023  recnz  9436  uzind  9454  eluzadd  9647  eluzsub  9648  ixxss1  9996  ixxss2  9997  ixxss12  9998  iccss2  10036  iccssioo2  10038  iccssico2  10039  elfzolt2  10249  infssuzcldc  10342  ioom  10367  elicore  10373  flqltp1  10386  addmodlteq  10507  expcl2lemap  10660  expap0i  10680  hashennnuni  10888  wrdexb  10964  crre  11039  caucvgre  11163  cvg1nlemcau  11166  cvg1nlemres  11167  resqrexlemoverl  11203  sqrtge0  11215  fimaxre2  11409  climi  11469  reccn2ap  11495  climge0  11507  nnf1o  11558  sumpr  11595  fsump1i  11615  fsum00  11644  fsumparts  11652  mertenslemi1  11717  addsin  11924  subsin  11925  addcos  11928  subcos  11929  sinbnd2  11936  cosbnd2  11937  sinltxirr  11943  dvdsaddre2b  12023  evenelz  12049  4dvdseven  12099  gcd0id  12171  gcd1  12179  bezoutlemstep  12189  dvdsgcdb  12205  mulgcd  12208  gcdzeq  12214  dvdsmulgcd  12217  sqgcd  12221  dvdssqlem  12222  bezoutr  12224  uzwodc  12229  nninfctlemfo  12232  lcmval  12256  lcmcllem  12260  lcmgcdlem  12270  lcmdvds  12272  lcmgcdeq  12276  lcmdvdsb  12277  mulgcddvds  12287  rpmulgcd2  12288  qredeu  12290  rpdvds  12292  divgcdcoprm0  12294  isprm3  12311  divgcdodd  12336  coprm  12337  rpexp  12346  sqrt2irr  12355  qdencl  12382  qeqnumdivden  12387  divnumden  12389  divdenle  12390  densq  12397  phimullem  12418  eulerthlem1  12420  eulerthlemrprm  12422  eulerthlemth  12425  prmdiveq  12429  prmdivdiv  12430  hashgcdeq  12433  phisum  12434  odzid  12438  reumodprminv  12447  oddn2prm  12455  pythagtriplem4  12462  pythagtriplem11  12468  pythagtriplem13  12470  pythagtriplem19  12476  pclemub  12481  pcprendvds2  12485  pcpre1  12486  pcpremul  12487  pceulem  12488  pczdvds  12508  pc2dvds  12524  pcaddlem  12533  pcmpt  12537  pcmpt2  12538  pcmptdvds  12539  pcprod  12540  pockthlem  12550  pockthg  12551  prmunb  12556  1arithlem4  12560  4sqlem7  12578  4sqlem8  12579  4sqlem9  12580  4sqlem10  12581  4sqlemffi  12590  4sqlem15  12599  4sqlem16  12600  4sqlem17  12601  4sqlem18  12602  ennnfonelemom  12650  ennnfonelemex  12656  ennnfonelemf1  12660  ctiunctlemu1st  12676  ctiunctlemu2nd  12677  fnpr2ob  13042  mgmlrid  13081  gsumfzval  13093  gsumval2  13099  mndrid  13138  prdsmndd  13150  grpinvcnv  13270  dfgrp3mlem  13300  prdsgrpd  13311  prdsinvgd  13312  eqglact  13431  ghmgrp2  13452  ghmlin  13454  ghmnsgpreima  13475  kerf1ghm  13480  srgdilem  13601  srgdir  13607  srgridm  13612  ringdilem  13644  ringdir  13651  ringridm  13656  unitmulcl  13745  unitnegcl  13762  rhmmhm  13791  elrhmunit  13809  lringuplu  13828  subrgring  13856  subrg1cl  13861  qusrhm  14160  znunit  14291  znrrg  14292  psrelbas  14304  inopn  14323  restbasg  14488  ssrest  14502  cntop2  14522  icnpimaex  14531  cnima  14540  lmfss  14564  lmtopcnp  14570  txhmeo  14639  txswaphmeo  14641  psmet0  14647  psmettri2  14648  blhalf  14728  bdxmet  14821  xmetxpbl  14828  ioo2bl  14871  tgioo  14874  cncfi  14898  rescncf  14901  cdivcncfap  14924  cnopnap  14931  divcncfap  14934  dedekindeulemeu  14942  dedekindicclemeu  14951  ivthinclemum  14955  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthinclemdisj  14960  ivthdec  14964  ivthreinc  14965  limcimo  14985  cnplimcim  14987  cnplimclemr  14989  cnlimci  14993  limccnpcntop  14995  limccnp2lem  14996  limccnp2cntop  14997  limccoap  14998  reldvg  14999  dvbsssg  15006  dvfgg  15008  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvrecap  15033  plyco  15079  plycj  15081  plyrecj  15083  sin0pilem1  15101  sin0pilem2  15102  tanrpcl  15157  tangtx  15158  cos0pilt1  15172  logbgcd1irraplemexp  15288  mpodvdsmulf1o  15310  perfect  15321  lgsne0  15363  lgseisen  15399  lgsquad2lem2  15407  2sqlem8a  15447  2sqlem8  15448  bj-charfunbi  15541  bj-inf2vnlem1  15700  pwf1oexmid  15730  subctctexmid  15731  iooref1o  15765  taupi  15804  alsi2d  15813  alsc2d  15815