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  998  simp3  999  sbh  1774  eldifbd  3139  unssbd  3311  opth  4231  potr  4302  frind  4346  brrelex2  4661  funinsn  5257  feu  5390  fcnvres  5391  fun11iun  5474  elmpocl2  6061  oprssdmm  6162  tfrlem1  6299  tfrlemisucfn  6315  tfrlemisucaccv  6316  tfrlemibxssdm  6318  tfrlemibfn  6319  tfrlemi14d  6324  swoer  6553  elmapssres  6663  mapsspm  6672  pmsspw  6673  mapss  6681  dom0  6828  xpf1o  6834  sbthlemi8  6953  sbthlemi9  6954  supelti  6991  supisoti  6999  djulclb  7044  nnnninfeq2  7117  cardcl  7170  isnumi  7171  cardval3ex  7174  exmidonfinlem  7182  en2eleq  7184  acfun  7196  exmidaclem  7197  ccfunen  7238  indpi  7316  dfplpq2  7328  ltbtwnnq  7390  enq0tr  7408  nqnq0pi  7412  elnp1st2nd  7450  prcunqu  7459  prnmaxl  7462  prloc  7465  genpcuu  7494  addnqprllem  7501  addlocprlemeq  7507  addlocprlemgt  7508  addlocpr  7510  nqprxx  7520  gtnqex  7524  appdivnq  7537  prmuloclemcalc  7539  prmuloc  7540  mullocprlem  7544  ltprordil  7563  ltnqpri  7568  ltexprlemm  7574  ltexprlemopl  7575  ltexprlemlol  7576  ltexprlemopu  7577  ltexprlemupu  7578  ltexprlemdisj  7580  ltexprlemloc  7581  ltexprlemfl  7583  ltexprlemrl  7584  ltexprlemfu  7585  ltexprlemru  7586  ltexpri  7587  recexprlemell  7596  recexprlemelu  7597  recexprlemloc  7605  recexprlempr  7606  recexprlem1ssl  7607  recexprlem1ssu  7608  recexprlemss1l  7609  aptipr  7615  cauappcvgprlemlol  7621  cauappcvgprlemupu  7623  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  cauappcvgprlemladdrl  7631  caucvgprlemnkj  7640  caucvgprlemnbj  7641  caucvgprlemlol  7644  caucvgprlemupu  7646  caucvgprlemladdfu  7651  caucvgprlem1  7653  caucvgprlem2  7654  caucvgprprlemnjltk  7665  caucvgprprlemnbj  7667  caucvgprprlemlol  7672  caucvgprprlemupu  7674  caucvgprprlemexbt  7680  caucvgprprlem1  7683  caucvgprprlem2  7684  suplocexprlemrl  7691  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemub  7697  suplocexprlemlub  7698  ltsrprg  7721  gt0srpr  7722  recexgt0sr  7747  addgt0sr  7749  mulgt0sr  7752  map2psrprg  7779  suplocsrlemb  7780  suplocsrlem  7782  nnindnn  7867  axcaucvglemcau  7872  axpre-suploclemres  7875  apreap  8518  apreim  8534  mulge0  8550  apti  8553  mulap0bbd  8590  lble  8877  nnind  8908  recnz  9319  uzind  9337  eluzadd  9529  eluzsub  9530  ixxss1  9875  ixxss2  9876  ixxss12  9877  iccss2  9915  iccssioo2  9917  iccssico2  9918  elfzolt2  10126  ioom  10231  elicore  10237  flqltp1  10249  addmodlteq  10368  expcl2lemap  10502  expap0i  10522  hashennnuni  10727  crre  10834  caucvgre  10958  cvg1nlemcau  10961  cvg1nlemres  10962  resqrexlemoverl  10998  sqrtge0  11010  fimaxre2  11203  climi  11263  reccn2ap  11289  climge0  11301  nnf1o  11352  sumpr  11389  fsump1i  11409  fsum00  11438  fsumparts  11446  mertenslemi1  11511  addsin  11718  subsin  11719  addcos  11722  subcos  11723  sinbnd2  11730  cosbnd2  11731  evenelz  11839  4dvdseven  11889  infssuzcldc  11919  gcd0id  11947  gcd1  11955  bezoutlemstep  11965  dvdsgcdb  11981  mulgcd  11984  gcdzeq  11990  dvdsmulgcd  11993  sqgcd  11997  dvdssqlem  11998  bezoutr  12000  uzwodc  12005  lcmval  12030  lcmcllem  12034  lcmgcdlem  12044  lcmdvds  12046  lcmgcdeq  12050  lcmdvdsb  12051  mulgcddvds  12061  rpmulgcd2  12062  qredeu  12064  rpdvds  12066  divgcdcoprm0  12068  isprm3  12085  divgcdodd  12110  coprm  12111  rpexp  12120  sqrt2irr  12129  qdencl  12156  qeqnumdivden  12161  divnumden  12163  divdenle  12164  densq  12171  phimullem  12192  eulerthlem1  12194  eulerthlemrprm  12196  eulerthlemth  12199  prmdiveq  12203  prmdivdiv  12204  hashgcdeq  12206  phisum  12207  odzid  12211  reumodprminv  12220  oddn2prm  12228  pythagtriplem4  12235  pythagtriplem11  12241  pythagtriplem13  12243  pythagtriplem19  12249  pclemub  12254  pcprendvds2  12258  pcpre1  12259  pcpremul  12260  pceulem  12261  pczdvds  12280  pc2dvds  12296  pcaddlem  12305  pcmpt  12308  pcmpt2  12309  pcmptdvds  12310  pcprod  12311  pockthlem  12321  pockthg  12322  prmunb  12327  1arithlem4  12331  4sqlem7  12349  4sqlem8  12350  4sqlem9  12351  4sqlem10  12352  ennnfonelemom  12376  ennnfonelemex  12382  ennnfonelemf1  12386  ctiunctlemu1st  12402  ctiunctlemu2nd  12403  mgmlrid  12664  mndrid  12703  grpinvcnv  12799  dfgrp3mlem  12829  srgdilem  12949  srgdir  12955  srgridm  12960  ringdilem  12992  ringdir  12999  ringridm  13004  inopn  13072  restbasg  13239  ssrest  13253  cntop2  13273  icnpimaex  13282  cnima  13291  lmfss  13315  lmtopcnp  13321  txhmeo  13390  txswaphmeo  13392  psmet0  13398  psmettri2  13399  blhalf  13479  bdxmet  13572  xmetxpbl  13579  ioo2bl  13614  tgioo  13617  cncfi  13636  rescncf  13639  cdivcncfap  13658  cnopnap  13665  dedekindeulemeu  13671  dedekindicclemeu  13680  ivthinclemum  13684  ivthinclemlopn  13685  ivthinclemuopn  13687  ivthinclemdisj  13689  ivthdec  13693  limcimo  13705  cnplimcim  13707  cnplimclemr  13709  cnlimci  13713  limccnpcntop  13715  limccnp2lem  13716  limccnp2cntop  13717  limccoap  13718  reldvg  13719  dvbsssg  13726  dvfgg  13728  dvaddxxbr  13736  dvmulxxbr  13737  dvcoapbr  13742  dvcjbr  13743  dvrecap  13748  sin0pilem1  13773  sin0pilem2  13774  tanrpcl  13829  tangtx  13830  cos0pilt1  13844  logbgcd1irraplemexp  13957  lgsne0  14010  2sqlem8a  14029  2sqlem8  14030  bj-charfunbi  14123  bj-inf2vnlem1  14282  pwf1oexmid  14309  subctctexmid  14311  iooref1o  14343  taupi  14379  alsi2d  14388  alsc2d  14390