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-mp 5  ax-1 6  ax-2 7  ax-ia2 106

This theorem is referenced by:  bi2  129  simprbi  273  simplbda  381  simp2  982  simp3  983  sbh  1749  eldifbd  3083  unssbd  3254  opth  4159  potr  4230  frind  4274  brrelex2  4580  funinsn  5172  feu  5305  fcnvres  5306  fun11iun  5388  elmpocl2  5970  oprssdmm  6069  tfrlem1  6205  tfrlemisucfn  6221  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemi14d  6230  swoer  6457  elmapssres  6567  mapsspm  6576  pmsspw  6577  mapss  6585  dom0  6732  xpf1o  6738  sbthlemi8  6852  sbthlemi9  6853  supelti  6889  supisoti  6897  djulclb  6940  cardcl  7037  isnumi  7038  cardval3ex  7041  exmidonfinlem  7049  en2eleq  7051  acfun  7063  exmidaclem  7064  ccfunen  7079  indpi  7150  dfplpq2  7162  ltbtwnnq  7224  enq0tr  7242  nqnq0pi  7246  elnp1st2nd  7284  prcunqu  7293  prnmaxl  7296  prloc  7299  genpcuu  7328  addnqprllem  7335  addlocprlemeq  7341  addlocprlemgt  7342  addlocpr  7344  nqprxx  7354  gtnqex  7358  appdivnq  7371  prmuloclemcalc  7373  prmuloc  7374  mullocprlem  7378  ltprordil  7397  ltnqpri  7402  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemfl  7417  ltexprlemrl  7418  ltexprlemfu  7419  ltexprlemru  7420  ltexpri  7421  recexprlemell  7430  recexprlemelu  7431  recexprlemloc  7439  recexprlempr  7440  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1l  7443  aptipr  7449  cauappcvgprlemlol  7455  cauappcvgprlemupu  7457  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdrl  7465  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemlol  7478  caucvgprlemupu  7480  caucvgprlemladdfu  7485  caucvgprlem1  7487  caucvgprlem2  7488  caucvgprprlemnjltk  7499  caucvgprprlemnbj  7501  caucvgprprlemlol  7506  caucvgprprlemupu  7508  caucvgprprlemexbt  7514  caucvgprprlem1  7517  caucvgprprlem2  7518  suplocexprlemrl  7525  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemub  7531  suplocexprlemlub  7532  ltsrprg  7555  gt0srpr  7556  recexgt0sr  7581  addgt0sr  7583  mulgt0sr  7586  map2psrprg  7613  suplocsrlemb  7614  suplocsrlem  7616  nnindnn  7701  axcaucvglemcau  7706  axpre-suploclemres  7709  apreap  8349  apreim  8365  mulge0  8381  apti  8384  mulap0bbd  8421  lble  8705  nnind  8736  recnz  9144  uzind  9162  eluzadd  9354  eluzsub  9355  ixxss1  9687  ixxss2  9688  ixxss12  9689  iccss2  9727  iccssioo2  9729  iccssico2  9730  elfzolt2  9933  ioom  10038  flqltp1  10052  addmodlteq  10171  expcl2lemap  10305  expap0i  10325  hashennnuni  10525  crre  10629  caucvgre  10753  cvg1nlemcau  10756  cvg1nlemres  10757  resqrexlemoverl  10793  sqrtge0  10805  fimaxre2  10998  climi  11056  reccn2ap  11082  climge0  11094  nnf1o  11145  sumpr  11182  fsump1i  11202  fsum00  11231  fsumparts  11239  mertenslemi1  11304  addsin  11449  subsin  11450  addcos  11453  subcos  11454  sinbnd2  11461  cosbnd2  11462  evenelz  11564  4dvdseven  11614  infssuzcldc  11644  gcd0id  11667  gcd1  11675  bezoutlemstep  11685  dvdsgcdb  11701  mulgcd  11704  gcdzeq  11710  dvdsmulgcd  11713  sqgcd  11717  dvdssqlem  11718  bezoutr  11720  lcmval  11744  lcmcllem  11748  lcmgcdlem  11758  lcmdvds  11760  lcmgcdeq  11764  lcmdvdsb  11765  mulgcddvds  11775  rpmulgcd2  11776  qredeu  11778  rpdvds  11780  divgcdcoprm0  11782  isprm3  11799  divgcdodd  11821  coprm  11822  rpexp  11831  sqrt2irr  11840  qdencl  11867  qeqnumdivden  11872  divnumden  11874  divdenle  11875  densq  11882  phimullem  11901  hashgcdeq  11904  ennnfonelemom  11921  ennnfonelemex  11927  ennnfonelemf1  11931  ctiunctlemu1st  11947  ctiunctlemu2nd  11948  inopn  12170  restbasg  12337  ssrest  12351  cntop2  12371  icnpimaex  12380  cnima  12389  lmfss  12413  lmtopcnp  12419  txhmeo  12488  txswaphmeo  12490  psmet0  12496  psmettri2  12497  blhalf  12577  bdxmet  12670  xmetxpbl  12677  ioo2bl  12712  tgioo  12715  cncfi  12734  rescncf  12737  cdivcncfap  12756  cnopnap  12763  dedekindeulemeu  12769  dedekindicclemeu  12778  ivthinclemum  12782  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthinclemdisj  12787  ivthdec  12791  limcimo  12803  cnplimcim  12805  cnplimclemr  12807  cnlimci  12811  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  limccoap  12816  reldvg  12817  dvbsssg  12824  dvfgg  12826  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvcjbr  12841  dvrecap  12846  sin0pilem1  12862  sin0pilem2  12863  tanrpcl  12918  tangtx  12919  bj-inf2vnlem1  13168  pwf1oexmid  13194  subctctexmid  13196  taupi  13239  alsi2d  13248  alsc2d  13250