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  1000  simp3  1001  sbh  1787  eldifbd  3166  unssbd  3338  opth  4267  potr  4340  frind  4384  brrelex2  4701  funinsn  5304  feu  5437  fcnvres  5438  fun11iun  5522  elmpocl2  6117  uchoice  6192  oprssdmm  6226  tfrlem1  6363  tfrlemisucfn  6379  tfrlemisucaccv  6380  tfrlemibxssdm  6382  tfrlemibfn  6383  tfrlemi14d  6388  swoer  6617  elmapssres  6729  mapsspm  6738  pmsspw  6739  mapss  6747  dom0  6896  xpf1o  6902  sbthlemi8  7025  sbthlemi9  7026  supelti  7063  supisoti  7071  djulclb  7116  nninfninc  7184  nnnninfeq2  7190  cardcl  7243  isnumi  7244  cardval3ex  7247  exmidonfinlem  7255  en2eleq  7257  acfun  7269  exmidaclem  7270  dftap2  7313  exmidapne  7322  ccfunen  7326  indpi  7404  dfplpq2  7416  ltbtwnnq  7478  enq0tr  7496  nqnq0pi  7500  elnp1st2nd  7538  prcunqu  7547  prnmaxl  7550  prloc  7553  genpcuu  7582  addnqprllem  7589  addlocprlemeq  7595  addlocprlemgt  7596  addlocpr  7598  nqprxx  7608  gtnqex  7612  appdivnq  7625  prmuloclemcalc  7627  prmuloc  7628  mullocprlem  7632  ltprordil  7651  ltnqpri  7656  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemfl  7671  ltexprlemrl  7672  ltexprlemfu  7673  ltexprlemru  7674  ltexpri  7675  recexprlemell  7684  recexprlemelu  7685  recexprlemloc  7693  recexprlempr  7694  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1l  7697  aptipr  7703  cauappcvgprlemlol  7709  cauappcvgprlemupu  7711  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdrl  7719  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemlol  7732  caucvgprlemupu  7734  caucvgprlemladdfu  7739  caucvgprlem1  7741  caucvgprlem2  7742  caucvgprprlemnjltk  7753  caucvgprprlemnbj  7755  caucvgprprlemlol  7760  caucvgprprlemupu  7762  caucvgprprlemexbt  7768  caucvgprprlem1  7771  caucvgprprlem2  7772  suplocexprlemrl  7779  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemub  7785  suplocexprlemlub  7786  ltsrprg  7809  gt0srpr  7810  recexgt0sr  7835  addgt0sr  7837  mulgt0sr  7840  map2psrprg  7867  suplocsrlemb  7868  suplocsrlem  7870  nnindnn  7955  axcaucvglemcau  7960  axpre-suploclemres  7963  apreap  8608  apreim  8624  mulge0  8640  apti  8643  mulap0bbd  8681  lble  8968  nnind  9000  recnz  9413  uzind  9431  eluzadd  9624  eluzsub  9625  ixxss1  9973  ixxss2  9974  ixxss12  9975  iccss2  10013  iccssioo2  10015  iccssico2  10016  elfzolt2  10226  ioom  10332  elicore  10338  flqltp1  10351  addmodlteq  10472  expcl2lemap  10625  expap0i  10645  hashennnuni  10853  wrdexb  10929  crre  11004  caucvgre  11128  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemoverl  11168  sqrtge0  11180  fimaxre2  11373  climi  11433  reccn2ap  11459  climge0  11471  nnf1o  11522  sumpr  11559  fsump1i  11579  fsum00  11608  fsumparts  11616  mertenslemi1  11681  addsin  11888  subsin  11889  addcos  11892  subcos  11893  sinbnd2  11900  cosbnd2  11901  sinltxirr  11907  dvdsaddre2b  11987  evenelz  12011  4dvdseven  12061  infssuzcldc  12091  gcd0id  12119  gcd1  12127  bezoutlemstep  12137  dvdsgcdb  12153  mulgcd  12156  gcdzeq  12162  dvdsmulgcd  12165  sqgcd  12169  dvdssqlem  12170  bezoutr  12172  uzwodc  12177  nninfctlemfo  12180  lcmval  12204  lcmcllem  12208  lcmgcdlem  12218  lcmdvds  12220  lcmgcdeq  12224  lcmdvdsb  12225  mulgcddvds  12235  rpmulgcd2  12236  qredeu  12238  rpdvds  12240  divgcdcoprm0  12242  isprm3  12259  divgcdodd  12284  coprm  12285  rpexp  12294  sqrt2irr  12303  qdencl  12330  qeqnumdivden  12335  divnumden  12337  divdenle  12338  densq  12345  phimullem  12366  eulerthlem1  12368  eulerthlemrprm  12370  eulerthlemth  12373  prmdiveq  12377  prmdivdiv  12378  hashgcdeq  12380  phisum  12381  odzid  12385  reumodprminv  12394  oddn2prm  12402  pythagtriplem4  12409  pythagtriplem11  12415  pythagtriplem13  12417  pythagtriplem19  12423  pclemub  12428  pcprendvds2  12432  pcpre1  12433  pcpremul  12434  pceulem  12435  pczdvds  12455  pc2dvds  12471  pcaddlem  12480  pcmpt  12484  pcmpt2  12485  pcmptdvds  12486  pcprod  12487  pockthlem  12497  pockthg  12498  prmunb  12503  1arithlem4  12507  4sqlem7  12525  4sqlem8  12526  4sqlem9  12527  4sqlem10  12528  4sqlemffi  12537  4sqlem15  12546  4sqlem16  12547  4sqlem17  12548  4sqlem18  12549  ennnfonelemom  12568  ennnfonelemex  12574  ennnfonelemf1  12578  ctiunctlemu1st  12594  ctiunctlemu2nd  12595  fnpr2ob  12926  mgmlrid  12965  gsumfzval  12977  gsumval2  12983  mndrid  13020  grpinvcnv  13143  dfgrp3mlem  13173  eqglact  13298  ghmgrp2  13319  ghmlin  13321  ghmnsgpreima  13342  kerf1ghm  13347  srgdilem  13468  srgdir  13474  srgridm  13479  ringdilem  13511  ringdir  13518  ringridm  13523  unitmulcl  13612  unitnegcl  13629  rhmmhm  13658  elrhmunit  13676  lringuplu  13695  subrgring  13723  subrg1cl  13728  qusrhm  14027  znunit  14158  znrrg  14159  psrelbas  14171  inopn  14182  restbasg  14347  ssrest  14361  cntop2  14381  icnpimaex  14390  cnima  14399  lmfss  14423  lmtopcnp  14429  txhmeo  14498  txswaphmeo  14500  psmet0  14506  psmettri2  14507  blhalf  14587  bdxmet  14680  xmetxpbl  14687  ioo2bl  14730  tgioo  14733  cncfi  14757  rescncf  14760  cdivcncfap  14783  cnopnap  14790  divcncfap  14793  dedekindeulemeu  14801  dedekindicclemeu  14810  ivthinclemum  14814  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthinclemdisj  14819  ivthdec  14823  ivthreinc  14824  limcimo  14844  cnplimcim  14846  cnplimclemr  14848  cnlimci  14852  limccnpcntop  14854  limccnp2lem  14855  limccnp2cntop  14856  limccoap  14857  reldvg  14858  dvbsssg  14865  dvfgg  14867  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvrecap  14892  plyco  14937  plycj  14939  plyrecj  14941  sin0pilem1  14957  sin0pilem2  14958  tanrpcl  15013  tangtx  15014  cos0pilt1  15028  logbgcd1irraplemexp  15141  lgsne0  15195  lgseisen  15231  lgsquad2lem2  15239  2sqlem8a  15279  2sqlem8  15280  bj-charfunbi  15373  bj-inf2vnlem1  15532  pwf1oexmid  15560  subctctexmid  15561  iooref1o  15594  taupi  15633  alsi2d  15642  alsc2d  15644