Theorem 3eqtr4d 2272

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4d	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4d

Step	Hyp	Ref	Expression
1		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eqtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
3		3eqtr4d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr4d 2265	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
5	1, 4	eqtr4d 2265	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  fnsnfv  5695  fvco2  5705  resfunexg  5864  fcof1  5913  fliftfun  5926  caovdir2d  6188  caov32d  6192  caov31d  6194  caov4d  6196  caovlem2d  6204  caofcom  6255  caofdig  6258  cnvf1olem  6376  tfrlem1  6460  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  frecrdg  6560  oav2  6617  omv2  6619  omsuc  6626  nnmsucr  6642  ecovicom  6798  ecoviass  6800  ecovidi  6802  nnnninfeq  7306  nninfwlpoimlemg  7353  carden2bex  7373  addcompig  7527  addasspig  7528  mulcompig  7529  mulasspig  7530  distrpig  7531  addassnqg  7580  addnq0mo  7645  mulnq0mo  7646  nqnq0a  7652  nqnq0m  7653  distrnq0  7657  mulcomnq0  7658  addassnq0  7660  addcmpblnr  7937  mulcmpblnrlemg  7938  addsrmo  7941  mulsrmo  7942  ltsrprg  7945  recexgt0sr  7971  mulgt0sr  7976  mulextsr1lem  7978  addcnsrec  8040  mulcnsrec  8041  pitonnlem2  8045  recidpirqlemcalc  8055  axaddcom  8068  adddir  8148  mul32  8287  mul31  8288  add32  8316  add4  8318  sub32  8391  sub4  8402  subdir  8543  mulneg2  8553  mulreim  8762  apadd1  8766  apneg  8769  divassap  8848  divdirap  8855  divmul13ap  8873  divmul24ap  8874  divdiv32ap  8878  conjmulap  8887  zeo  9563  xaddcom  10069  xnegdi  10076  xaddass  10077  xaddass2  10078  xpncan  10079  xadd4d  10093  lincmb01cmp  10211  iccf1o  10212  flhalf  10534  modqvalp1  10577  modqdi  10626  modqsubdir  10627  frecuzrdgg  10650  seq3shft2  10715  seqshft2g  10716  seq3caopr3  10725  seqcaopr3g  10726  seq3caopr  10729  seqcaoprg  10730  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seqf1oglem2a  10752  seqf1oglem2  10754  seqf1og  10755  seq3homo  10761  seqfeq3  10763  seqhomog  10764  seqfeq4g  10765  seq3distr  10766  expp1  10780  expnegap0  10781  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  sqneg  10832  sqdivap  10837  subsq2  10881  binom2  10885  modqexp  10900  facp1  10964  bcm1k  10994  bcp1n  10995  bcval5  10997  omgadd  11036  hashun  11039  hashxp  11061  csbwrdg  11114  ccatass  11156  lswccatn0lsw  11159  swrdlsw  11216  swrdswrd  11252  wrd2ind  11270  swrdccatin1  11272  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12lem3  11279  pfxccatpfx1  11283  swrdccat3blem  11286  cats1catd  11315  shftfibg  11346  shftfib  11349  shftval  11351  2shfti  11357  seq3shft  11364  crre  11383  remim  11386  mulreap  11390  reneg  11394  readd  11395  remullem  11397  redivap  11400  imneg  11402  imadd  11403  imdivap  11407  cjcj  11409  cjadd  11410  cjmulrcl  11413  cjneg  11416  imval2  11420  resqrexlemcalc1  11540  absneg  11576  sqabsadd  11581  sqabssub  11582  absmul  11595  absresq  11604  absexp  11605  absexpzap  11606  bdtrilem  11765  xrmaxiflemcom  11775  xrmaxadd  11787  xrminrecl  11799  xrminadd  11801  serf0  11878  summodclem3  11906  fsum3  11913  isumss  11917  fisumss  11918  fsumadd  11932  isummulc1  11953  isumdivapc  11954  fsum2dlemstep  11960  fisumcom2  11964  fisum0diag2  11973  fsummulc2  11974  fsummulc1  11975  fsumdivapc  11976  fsumconst  11980  telfsumo  11992  fsumparts  11996  binomlem  12009  isumshft  12016  arisum2  12025  geolim  12037  geo2sum  12040  geo2lim  12042  cvgratnnlemseq  12052  cvgratz  12058  mertenslem2  12062  prodfrecap  12072  prodfdivap  12073  prodmodclem2a  12102  fprodntrivap  12110  fprodssdc  12116  fprodmul  12117  fprodabs  12142  fprod2dlemstep  12148  fprodcom2fi  12152  fprodrec  12155  efcllemp  12184  efcj  12199  efexp  12208  resinval  12241  recosval  12242  cosneg  12253  efival  12258  sinadd  12262  cosadd  12263  addcos  12272  sin2t  12275  cos2t  12276  dvdsmodexp  12321  odd2np1lem  12398  oexpneg  12403  neggcd  12519  gcdabs2  12526  mulgcd  12552  mulgcdr  12554  gcddiv  12555  rplpwr  12563  eucalgval  12591  eucalginv  12593  eucalg  12596  neglcm  12612  lcmgcd  12615  mulgcddvds  12631  qredeu  12634  nn0gcdsq  12737  phimullem  12762  prmdiv  12772  coprimeprodsq  12795  pythagtriplem1  12803  pythagtriplem3  12805  pythagtriplem4  12806  pythagtriplem12  12813  pceulem  12832  pceu  12833  pcqmul  12841  pcexp  12847  pcneg  12863  pcadd  12878  pcmpt  12881  pcmpt2  12882  pcbc  12889  4sqlem7  12922  4sqlem10  12925  mul4sqlem  12931  4sqlem11  12939  ennnfonelemp1  12992  setsabsd  13086  setscom  13087  ressbasd  13115  strressid  13119  ressinbasd  13122  ressressg  13123  ressplusgd  13177  prdsval  13321  pwsplusgval  13343  pwsmulrval  13344  imasival  13354  qusin  13374  fvprif  13391  xpsfeq  13393  grpidpropdg  13422  gsumpropd  13440  gsumpropd2  13441  gsumress  13443  prdssgrpd  13463  mnd32g  13475  mnd4g  13477  prdsidlem  13495  prdsmndd  13496  pws0g  13499  imasmnd2  13500  0mhm  13534  resmhm  13535  mhmco  13538  gsumwmhm  13546  grpinvcnv  13616  grpinvpropdg  13623  grpinvsub  13630  grpaddsubass  13638  grpsubpropdg  13652  grpsubpropd2  13653  prdsinvlem  13656  pwsinvg  13660  pwssub  13661  imasgrp2  13662  imasgrp  13663  qusgrp2  13665  mulgnnp1  13682  mulgnegnn  13684  mulgaddcom  13698  mulginvcom  13699  mulgnndir  13703  mulgnn0ass  13710  mhmmulg  13715  mulgpropdg  13716  submmulg  13718  subginv  13733  subgsub  13738  subgmulg  13740  eqglact  13777  ghmsub  13803  ghmmulg  13808  resghm  13812  ghmeql  13819  conjghm  13828  ablsub4  13865  ablsub32  13874  imasabl  13888  gsumfzreidx  13889  gsumfzmptfidmadd  13891  gsumfzconst  13893  mgpress  13909  rngsubdi  13929  rngsubdir  13930  imasrng  13934  dfur2g  13940  srgass  13949  srgmulgass  13967  srgpcomp  13968  srglmhm  13971  srgrmhm  13972  crngcom  13992  ringass  13994  ringcom  14009  ringsubdi  14034  ringsubdir  14035  mulgass2  14036  ringlghm  14039  ringrghm  14040  imasring  14042  opprrng  14055  opprring  14057  oppr0g  14059  oppr1g  14060  opprnegg  14061  mulgass3  14063  dvdsrvald  14072  unitlinv  14105  unitrinv  14106  dvrfvald  14112  dvrass  14118  dvrdir  14122  rdivmuldivd  14123  rngidpropdg  14125  dvdsrpropdg  14126  unitpropdg  14127  invrpropdg  14128  rhm1  14146  rhmopp  14155  subrguss  14215  subrginv  14216  subrgdv  14217  lmodcom  14312  lmodsubdir  14324  rmodislmod  14330  lsppropd  14411  srascag  14421  sravscag  14422  ixpsnbasval  14445  rsp0  14472  lidlrsppropdg  14474  rnglidlmsgrp  14476  gsumfzfsumlemm  14566  expghmap  14586  mulgghm2  14587  mulgrhm  14588  zlmlemg  14607  zlmsca  14611  znle  14616  psrbasg  14653  psrplusgg  14657  psrlinv  14663  tgdom  14761  txbasval  14956  cnmpt11  14972  cnmpt21  14980  setsmsbasg  15168  bdbl  15192  dvmulxxbr  15391  dvimulf  15395  dvcj  15398  dvfre  15399  dvrecap  15402  dvmptc  15406  dvmptfsum  15414  dvef  15416  plyaddlem1  15436  plyrecj  15452  dvply1  15454  sinperlem  15497  coshalfpip  15511  ptolemy  15513  tangtx  15527  relogef  15553  rpcxpadd  15594  rpmulcxp  15598  rpdivcxp  15600  cxpmul  15601  rpcxpmul2  15602  abscxp  15604  rpcxpsqrt  15611  rpabscxpbnd  15629  rplogbreexp  15642  rprelogbmul  15644  rprelogbdiv  15646  1sgmprm  15683  perfect1  15687  perfectlem2  15689  perfect  15690  lgsneg  15718  lgsmod  15720  lgsdir2  15727  lgsdirprm  15728  lgsdir  15729  lgsdi  15731  lgssq  15734  lgssq2  15735  lgsdirnn0  15741  lgsdinn0  15742  gausslemma2dlem6  15761  lgseisenlem1  15764  lgseisenlem3  15766  lgseisenlem4  15767  lgsquadlem1  15771  lgsquad2  15777  2sqlem3  15811  setsiedg  15868  vtxdeqd  16055  vtxdfifiun  16056  bj-charfundcALT  16227  nninfsellemeqinf  16442  refeq  16456