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  987  simp3  988  sbh  1763  eldifbd  3123  unssbd  3295  opth  4209  potr  4280  frind  4324  brrelex2  4639  funinsn  5231  feu  5364  fcnvres  5365  fun11iun  5447  elmpocl2  6032  oprssdmm  6131  tfrlem1  6267  tfrlemisucfn  6283  tfrlemisucaccv  6284  tfrlemibxssdm  6286  tfrlemibfn  6287  tfrlemi14d  6292  swoer  6520  elmapssres  6630  mapsspm  6639  pmsspw  6640  mapss  6648  dom0  6795  xpf1o  6801  sbthlemi8  6920  sbthlemi9  6921  supelti  6958  supisoti  6966  djulclb  7011  nnnninfeq2  7084  cardcl  7128  isnumi  7129  cardval3ex  7132  exmidonfinlem  7140  en2eleq  7142  acfun  7154  exmidaclem  7155  ccfunen  7196  indpi  7274  dfplpq2  7286  ltbtwnnq  7348  enq0tr  7366  nqnq0pi  7370  elnp1st2nd  7408  prcunqu  7417  prnmaxl  7420  prloc  7423  genpcuu  7452  addnqprllem  7459  addlocprlemeq  7465  addlocprlemgt  7466  addlocpr  7468  nqprxx  7478  gtnqex  7482  appdivnq  7495  prmuloclemcalc  7497  prmuloc  7498  mullocprlem  7502  ltprordil  7521  ltnqpri  7526  ltexprlemm  7532  ltexprlemopl  7533  ltexprlemlol  7534  ltexprlemopu  7535  ltexprlemupu  7536  ltexprlemdisj  7538  ltexprlemloc  7539  ltexprlemfl  7541  ltexprlemrl  7542  ltexprlemfu  7543  ltexprlemru  7544  ltexpri  7545  recexprlemell  7554  recexprlemelu  7555  recexprlemloc  7563  recexprlempr  7564  recexprlem1ssl  7565  recexprlem1ssu  7566  recexprlemss1l  7567  aptipr  7573  cauappcvgprlemlol  7579  cauappcvgprlemupu  7581  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  cauappcvgprlemladdrl  7589  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemlol  7602  caucvgprlemupu  7604  caucvgprlemladdfu  7609  caucvgprlem1  7611  caucvgprlem2  7612  caucvgprprlemnjltk  7623  caucvgprprlemnbj  7625  caucvgprprlemlol  7630  caucvgprprlemupu  7632  caucvgprprlemexbt  7638  caucvgprprlem1  7641  caucvgprprlem2  7642  suplocexprlemrl  7649  suplocexprlemru  7651  suplocexprlemdisj  7652  suplocexprlemub  7655  suplocexprlemlub  7656  ltsrprg  7679  gt0srpr  7680  recexgt0sr  7705  addgt0sr  7707  mulgt0sr  7710  map2psrprg  7737  suplocsrlemb  7738  suplocsrlem  7740  nnindnn  7825  axcaucvglemcau  7830  axpre-suploclemres  7833  apreap  8476  apreim  8492  mulge0  8508  apti  8511  mulap0bbd  8548  lble  8833  nnind  8864  recnz  9275  uzind  9293  eluzadd  9485  eluzsub  9486  ixxss1  9831  ixxss2  9832  ixxss12  9833  iccss2  9871  iccssioo2  9873  iccssico2  9874  elfzolt2  10081  ioom  10186  elicore  10192  flqltp1  10204  addmodlteq  10323  expcl2lemap  10457  expap0i  10477  hashennnuni  10681  crre  10785  caucvgre  10909  cvg1nlemcau  10912  cvg1nlemres  10913  resqrexlemoverl  10949  sqrtge0  10961  fimaxre2  11154  climi  11214  reccn2ap  11240  climge0  11252  nnf1o  11303  sumpr  11340  fsump1i  11360  fsum00  11389  fsumparts  11397  mertenslemi1  11462  addsin  11669  subsin  11670  addcos  11673  subcos  11674  sinbnd2  11681  cosbnd2  11682  evenelz  11789  4dvdseven  11839  infssuzcldc  11869  gcd0id  11897  gcd1  11905  bezoutlemstep  11915  dvdsgcdb  11931  mulgcd  11934  gcdzeq  11940  dvdsmulgcd  11943  sqgcd  11947  dvdssqlem  11948  bezoutr  11950  lcmval  11974  lcmcllem  11978  lcmgcdlem  11988  lcmdvds  11990  lcmgcdeq  11994  lcmdvdsb  11995  mulgcddvds  12005  rpmulgcd2  12006  qredeu  12008  rpdvds  12010  divgcdcoprm0  12012  isprm3  12029  divgcdodd  12052  coprm  12053  rpexp  12062  sqrt2irr  12071  qdencl  12098  qeqnumdivden  12103  divnumden  12105  divdenle  12106  densq  12113  phimullem  12134  eulerthlem1  12136  eulerthlemrprm  12138  eulerthlemth  12141  prmdiveq  12145  prmdivdiv  12146  hashgcdeq  12148  phisum  12149  odzid  12153  reumodprminv  12162  oddn2prm  12170  pythagtriplem4  12177  pythagtriplem11  12183  pythagtriplem13  12185  pythagtriplem19  12191  pclemub  12196  pcprendvds2  12200  pcpre1  12201  pcpremul  12202  pceulem  12203  pczdvds  12222  pc2dvds  12238  pcaddlem  12247  pcmpt  12250  pcmpt2  12251  pcmptdvds  12252  pcprod  12253  ennnfonelemom  12278  ennnfonelemex  12284  ennnfonelemf1  12288  ctiunctlemu1st  12304  ctiunctlemu2nd  12305  inopn  12542  restbasg  12709  ssrest  12723  cntop2  12743  icnpimaex  12752  cnima  12761  lmfss  12785  lmtopcnp  12791  txhmeo  12860  txswaphmeo  12862  psmet0  12868  psmettri2  12869  blhalf  12949  bdxmet  13042  xmetxpbl  13049  ioo2bl  13084  tgioo  13087  cncfi  13106  rescncf  13109  cdivcncfap  13128  cnopnap  13135  dedekindeulemeu  13141  dedekindicclemeu  13150  ivthinclemum  13154  ivthinclemlopn  13155  ivthinclemuopn  13157  ivthinclemdisj  13159  ivthdec  13163  limcimo  13175  cnplimcim  13177  cnplimclemr  13179  cnlimci  13183  limccnpcntop  13185  limccnp2lem  13186  limccnp2cntop  13187  limccoap  13188  reldvg  13189  dvbsssg  13196  dvfgg  13198  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvcjbr  13213  dvrecap  13218  sin0pilem1  13243  sin0pilem2  13244  tanrpcl  13299  tangtx  13300  cos0pilt1  13314  logbgcd1irraplemexp  13427  bj-charfunbi  13528  bj-inf2vnlem1  13687  pwf1oexmid  13713  subctctexmid  13715  iooref1o  13747  taupi  13783  alsi2d  13792  alsc2d  13794