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:  biimpr  129  simprbi  273  simplbda  382  simp2  988  simp3  989  sbh  1764  eldifbd  3128  unssbd  3300  opth  4215  potr  4286  frind  4330  brrelex2  4645  funinsn  5237  feu  5370  fcnvres  5371  fun11iun  5453  elmpocl2  6038  oprssdmm  6139  tfrlem1  6276  tfrlemisucfn  6292  tfrlemisucaccv  6293  tfrlemibxssdm  6295  tfrlemibfn  6296  tfrlemi14d  6301  swoer  6529  elmapssres  6639  mapsspm  6648  pmsspw  6649  mapss  6657  dom0  6804  xpf1o  6810  sbthlemi8  6929  sbthlemi9  6930  supelti  6967  supisoti  6975  djulclb  7020  nnnninfeq2  7093  cardcl  7137  isnumi  7138  cardval3ex  7141  exmidonfinlem  7149  en2eleq  7151  acfun  7163  exmidaclem  7164  ccfunen  7205  indpi  7283  dfplpq2  7295  ltbtwnnq  7357  enq0tr  7375  nqnq0pi  7379  elnp1st2nd  7417  prcunqu  7426  prnmaxl  7429  prloc  7432  genpcuu  7461  addnqprllem  7468  addlocprlemeq  7474  addlocprlemgt  7475  addlocpr  7477  nqprxx  7487  gtnqex  7491  appdivnq  7504  prmuloclemcalc  7506  prmuloc  7507  mullocprlem  7511  ltprordil  7530  ltnqpri  7535  ltexprlemm  7541  ltexprlemopl  7542  ltexprlemlol  7543  ltexprlemopu  7544  ltexprlemupu  7545  ltexprlemdisj  7547  ltexprlemloc  7548  ltexprlemfl  7550  ltexprlemrl  7551  ltexprlemfu  7552  ltexprlemru  7553  ltexpri  7554  recexprlemell  7563  recexprlemelu  7564  recexprlemloc  7572  recexprlempr  7573  recexprlem1ssl  7574  recexprlem1ssu  7575  recexprlemss1l  7576  aptipr  7582  cauappcvgprlemlol  7588  cauappcvgprlemupu  7590  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlemladdrl  7598  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemlol  7611  caucvgprlemupu  7613  caucvgprlemladdfu  7618  caucvgprlem1  7620  caucvgprlem2  7621  caucvgprprlemnjltk  7632  caucvgprprlemnbj  7634  caucvgprprlemlol  7639  caucvgprprlemupu  7641  caucvgprprlemexbt  7647  caucvgprprlem1  7650  caucvgprprlem2  7651  suplocexprlemrl  7658  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemub  7664  suplocexprlemlub  7665  ltsrprg  7688  gt0srpr  7689  recexgt0sr  7714  addgt0sr  7716  mulgt0sr  7719  map2psrprg  7746  suplocsrlemb  7747  suplocsrlem  7749  nnindnn  7834  axcaucvglemcau  7839  axpre-suploclemres  7842  apreap  8485  apreim  8501  mulge0  8517  apti  8520  mulap0bbd  8557  lble  8842  nnind  8873  recnz  9284  uzind  9302  eluzadd  9494  eluzsub  9495  ixxss1  9840  ixxss2  9841  ixxss12  9842  iccss2  9880  iccssioo2  9882  iccssico2  9883  elfzolt2  10091  ioom  10196  elicore  10202  flqltp1  10214  addmodlteq  10333  expcl2lemap  10467  expap0i  10487  hashennnuni  10692  crre  10799  caucvgre  10923  cvg1nlemcau  10926  cvg1nlemres  10927  resqrexlemoverl  10963  sqrtge0  10975  fimaxre2  11168  climi  11228  reccn2ap  11254  climge0  11266  nnf1o  11317  sumpr  11354  fsump1i  11374  fsum00  11403  fsumparts  11411  mertenslemi1  11476  addsin  11683  subsin  11684  addcos  11687  subcos  11688  sinbnd2  11695  cosbnd2  11696  evenelz  11804  4dvdseven  11854  infssuzcldc  11884  gcd0id  11912  gcd1  11920  bezoutlemstep  11930  dvdsgcdb  11946  mulgcd  11949  gcdzeq  11955  dvdsmulgcd  11958  sqgcd  11962  dvdssqlem  11963  bezoutr  11965  uzwodc  11970  lcmval  11995  lcmcllem  11999  lcmgcdlem  12009  lcmdvds  12011  lcmgcdeq  12015  lcmdvdsb  12016  mulgcddvds  12026  rpmulgcd2  12027  qredeu  12029  rpdvds  12031  divgcdcoprm0  12033  isprm3  12050  divgcdodd  12075  coprm  12076  rpexp  12085  sqrt2irr  12094  qdencl  12121  qeqnumdivden  12126  divnumden  12128  divdenle  12129  densq  12136  phimullem  12157  eulerthlem1  12159  eulerthlemrprm  12161  eulerthlemth  12164  prmdiveq  12168  prmdivdiv  12169  hashgcdeq  12171  phisum  12172  odzid  12176  reumodprminv  12185  oddn2prm  12193  pythagtriplem4  12200  pythagtriplem11  12206  pythagtriplem13  12208  pythagtriplem19  12214  pclemub  12219  pcprendvds2  12223  pcpre1  12224  pcpremul  12225  pceulem  12226  pczdvds  12245  pc2dvds  12261  pcaddlem  12270  pcmpt  12273  pcmpt2  12274  pcmptdvds  12275  pcprod  12276  pockthlem  12286  pockthg  12287  prmunb  12292  1arithlem4  12296  4sqlem7  12314  4sqlem8  12315  4sqlem9  12316  4sqlem10  12317  ennnfonelemom  12341  ennnfonelemex  12347  ennnfonelemf1  12351  ctiunctlemu1st  12367  ctiunctlemu2nd  12368  mgmlrid  12610  inopn  12641  restbasg  12808  ssrest  12822  cntop2  12842  icnpimaex  12851  cnima  12860  lmfss  12884  lmtopcnp  12890  txhmeo  12959  txswaphmeo  12961  psmet0  12967  psmettri2  12968  blhalf  13048  bdxmet  13141  xmetxpbl  13148  ioo2bl  13183  tgioo  13186  cncfi  13205  rescncf  13208  cdivcncfap  13227  cnopnap  13234  dedekindeulemeu  13240  dedekindicclemeu  13249  ivthinclemum  13253  ivthinclemlopn  13254  ivthinclemuopn  13256  ivthinclemdisj  13258  ivthdec  13262  limcimo  13274  cnplimcim  13276  cnplimclemr  13278  cnlimci  13282  limccnpcntop  13284  limccnp2lem  13285  limccnp2cntop  13286  limccoap  13287  reldvg  13288  dvbsssg  13295  dvfgg  13297  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvcjbr  13312  dvrecap  13317  sin0pilem1  13342  sin0pilem2  13343  tanrpcl  13398  tangtx  13399  cos0pilt1  13413  logbgcd1irraplemexp  13526  lgsne0  13579  2sqlem8a  13598  2sqlem8  13599  bj-charfunbi  13693  bj-inf2vnlem1  13852  pwf1oexmid  13879  subctctexmid  13881  iooref1o  13913  taupi  13949  alsi2d  13958  alsc2d  13960