Theorem simprd 113

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 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 106

This theorem is referenced by:  bi2  129  simprbi  271  simplbda  379  simp2  950  simp3  951  sbh  1717  eldifbd  3033  unssbd  3201  opth  4097  potr  4168  frind  4212  brrelex2  4518  funinsn  5108  feu  5241  fcnvres  5242  fun11iun  5322  elmpocl2  5902  tfrlem1  6135  tfrlemisucfn  6151  tfrlemisucaccv  6152  tfrlemibxssdm  6154  tfrlemibfn  6155  tfrlemi14d  6160  swoer  6387  elmapssres  6497  mapsspm  6506  pmsspw  6507  mapss  6515  dom0  6661  xpf1o  6667  sbthlemi8  6780  sbthlemi9  6781  supelti  6804  supisoti  6812  djulclb  6855  cardcl  6948  isnumi  6949  cardval3ex  6952  en2eleq  6960  indpi  7051  dfplpq2  7063  ltbtwnnq  7125  enq0tr  7143  nqnq0pi  7147  elnp1st2nd  7185  prcunqu  7194  prnmaxl  7197  prloc  7200  genpcuu  7229  addnqprllem  7236  addlocprlemeq  7242  addlocprlemgt  7243  addlocpr  7245  nqprxx  7255  gtnqex  7259  appdivnq  7272  prmuloclemcalc  7274  prmuloc  7275  mullocprlem  7279  ltprordil  7298  ltnqpri  7303  ltexprlemm  7309  ltexprlemopl  7310  ltexprlemlol  7311  ltexprlemopu  7312  ltexprlemupu  7313  ltexprlemdisj  7315  ltexprlemloc  7316  ltexprlemfl  7318  ltexprlemrl  7319  ltexprlemfu  7320  ltexprlemru  7321  ltexpri  7322  recexprlemell  7331  recexprlemelu  7332  recexprlemloc  7340  recexprlempr  7341  recexprlem1ssl  7342  recexprlem1ssu  7343  recexprlemss1l  7344  aptipr  7350  cauappcvgprlemlol  7356  cauappcvgprlemupu  7358  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  cauappcvgprlemladdrl  7366  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemlol  7379  caucvgprlemupu  7381  caucvgprlemladdfu  7386  caucvgprlem1  7388  caucvgprlem2  7389  caucvgprprlemnjltk  7400  caucvgprprlemnbj  7402  caucvgprprlemlol  7407  caucvgprprlemupu  7409  caucvgprprlemexbt  7415  caucvgprprlem1  7418  caucvgprprlem2  7419  ltsrprg  7443  gt0srpr  7444  recexgt0sr  7469  addgt0sr  7471  mulgt0sr  7473  nnindnn  7578  axcaucvglemcau  7583  apreap  8215  apreim  8231  mulge0  8247  apti  8250  mulap0bbd  8282  lble  8563  nnind  8594  recnz  8996  uzind  9014  eluzadd  9204  eluzsub  9205  ixxss1  9528  ixxss2  9529  ixxss12  9530  iccss2  9568  iccssioo2  9570  iccssico2  9571  elfzolt2  9774  ioom  9879  flqltp1  9893  addmodlteq  10012  expcl2lemap  10146  expap0i  10166  hashennnuni  10366  crre  10470  caucvgre  10593  cvg1nlemcau  10596  cvg1nlemres  10597  resqrexlemoverl  10633  sqrtge0  10645  fimaxre2  10837  climi  10895  reccn2ap  10921  climge0  10933  isummolemnm  10987  sumpr  11021  fsump1i  11041  fsum00  11070  fsumparts  11078  mertenslemi1  11143  addsin  11247  subsin  11248  addcos  11251  subcos  11252  sinbnd2  11259  cosbnd2  11260  evenelz  11359  4dvdseven  11409  infssuzcldc  11439  gcd0id  11462  gcd1  11470  bezoutlemstep  11478  dvdsgcdb  11494  mulgcd  11497  gcdzeq  11503  dvdsmulgcd  11506  sqgcd  11510  dvdssqlem  11511  bezoutr  11513  lcmval  11537  lcmcllem  11541  lcmgcdlem  11551  lcmdvds  11553  lcmgcdeq  11557  lcmdvdsb  11558  mulgcddvds  11568  rpmulgcd2  11569  qredeu  11571  rpdvds  11573  divgcdcoprm0  11575  isprm3  11592  divgcdodd  11614  coprm  11615  rpexp  11624  sqrt2irr  11633  qdencl  11659  qeqnumdivden  11664  divnumden  11666  divdenle  11667  densq  11674  phimullem  11693  hashgcdeq  11696  ennnfonelemom  11713  ennnfonelemex  11719  ennnfonelemf1  11723  inopn  11952  restbasg  12119  ssrest  12133  cntop2  12152  icnpimaex  12161  cnima  12170  lmfss  12194  lmtopcnp  12200  psmet0  12255  psmettri2  12256  blhalf  12336  bdxmet  12429  ioo2bl  12462  tgioo  12465  cncfi  12478  rescncf  12481  cdivcncfap  12499  limcimo  12514  cnplimcim  12516  cnlimci  12518  limccnpcntop  12520  reldvg  12521  dvbsssg  12528  dvfgg  12530  bj-inf2vnlem1  12753  pwf1oexmid  12780  alsi2d  12830  alsc2d  12832