Theorem 3eqtr4d 2274

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 2267	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
5	1, 4	eqtr4d 2267	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  fnsnfv  5714  fvco2  5724  resfunexg  5883  fcof1  5934  fliftfun  5947  caovdir2d  6209  caov32d  6213  caov31d  6215  caov4d  6217  caovlem2d  6225  caofcom  6275  caofdig  6278  cnvf1olem  6398  tfrlem1  6517  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  frecrdg  6617  oav2  6674  omv2  6676  omsuc  6683  nnmsucr  6699  ecovicom  6855  ecoviass  6857  ecovidi  6859  nnnninfeq  7370  nninfwlpoimlemg  7417  carden2bex  7437  addcompig  7592  addasspig  7593  mulcompig  7594  mulasspig  7595  distrpig  7596  addassnqg  7645  addnq0mo  7710  mulnq0mo  7711  nqnq0a  7717  nqnq0m  7718  distrnq0  7722  mulcomnq0  7723  addassnq0  7725  addcmpblnr  8002  mulcmpblnrlemg  8003  addsrmo  8006  mulsrmo  8007  ltsrprg  8010  recexgt0sr  8036  mulgt0sr  8041  mulextsr1lem  8043  addcnsrec  8105  mulcnsrec  8106  pitonnlem2  8110  recidpirqlemcalc  8120  axaddcom  8133  adddir  8213  mul32  8351  mul31  8352  add32  8380  add4  8382  sub32  8455  sub4  8466  subdir  8607  mulneg2  8617  mulreim  8826  apadd1  8830  apneg  8833  divassap  8912  divdirap  8919  divmul13ap  8937  divmul24ap  8938  divdiv32ap  8942  conjmulap  8951  zeo  9629  xaddcom  10140  xnegdi  10147  xaddass  10148  xaddass2  10149  xpncan  10150  xadd4d  10164  lincmb01cmp  10282  iccf1o  10284  flhalf  10608  modqvalp1  10651  modqdi  10700  modqsubdir  10701  frecuzrdgg  10724  seq3shft2  10789  seqshft2g  10790  seq3caopr3  10799  seqcaopr3g  10800  seq3caopr  10803  seqcaoprg  10804  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seq3f1olemqsum  10821  seqf1oglem2a  10826  seqf1oglem2  10828  seqf1og  10829  seq3homo  10835  seqfeq3  10837  seqhomog  10838  seqfeq4g  10839  seq3distr  10840  expp1  10854  expnegap0  10855  expaddzaplem  10890  expaddzap  10891  expmulzap  10893  sqneg  10906  sqdivap  10911  subsq2  10955  binom2  10959  modqexp  10974  facp1  11038  bcm1k  11068  bcp1n  11069  bcval5  11071  omgadd  11111  hashun  11114  hashxp  11136  csbwrdg  11192  ccatass  11234  lswccatn0lsw  11237  swrdlsw  11299  swrdswrd  11335  wrd2ind  11353  swrdccatin1  11355  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12lem3  11362  pfxccatpfx1  11366  swrdccat3blem  11369  cats1catd  11398  shftfibg  11443  shftfib  11446  shftval  11448  2shfti  11454  seq3shft  11461  crre  11480  remim  11483  mulreap  11487  reneg  11491  readd  11492  remullem  11494  redivap  11497  imneg  11499  imadd  11500  imdivap  11504  cjcj  11506  cjadd  11507  cjmulrcl  11510  cjneg  11513  imval2  11517  resqrexlemcalc1  11637  absneg  11673  sqabsadd  11678  sqabssub  11679  absmul  11692  absresq  11701  absexp  11702  absexpzap  11703  bdtrilem  11862  xrmaxiflemcom  11872  xrmaxadd  11884  xrminrecl  11896  xrminadd  11898  serf0  11975  summodclem3  12004  fsum3  12011  isumss  12015  fisumss  12016  fsumadd  12030  isummulc1  12051  isumdivapc  12052  fsum2dlemstep  12058  fisumcom2  12062  fisum0diag2  12071  fsummulc2  12072  fsummulc1  12073  fsumdivapc  12074  fsumconst  12078  telfsumo  12090  fsumparts  12094  binomlem  12107  isumshft  12114  arisum2  12123  geolim  12135  geo2sum  12138  geo2lim  12140  cvgratnnlemseq  12150  cvgratz  12156  mertenslem2  12160  prodfrecap  12170  prodfdivap  12171  prodmodclem2a  12200  fprodntrivap  12208  fprodssdc  12214  fprodmul  12215  fprodabs  12240  fprod2dlemstep  12246  fprodcom2fi  12250  fprodrec  12253  efcllemp  12282  efcj  12297  efexp  12306  resinval  12339  recosval  12340  cosneg  12351  efival  12356  sinadd  12360  cosadd  12361  addcos  12370  sin2t  12373  cos2t  12374  dvdsmodexp  12419  odd2np1lem  12496  oexpneg  12501  neggcd  12617  gcdabs2  12624  mulgcd  12650  mulgcdr  12652  gcddiv  12653  rplpwr  12661  eucalgval  12689  eucalginv  12691  eucalg  12694  neglcm  12710  lcmgcd  12713  mulgcddvds  12729  qredeu  12732  nn0gcdsq  12835  phimullem  12860  prmdiv  12870  coprimeprodsq  12893  pythagtriplem1  12901  pythagtriplem3  12903  pythagtriplem4  12904  pythagtriplem12  12911  pceulem  12930  pceu  12931  pcqmul  12939  pcexp  12945  pcneg  12961  pcadd  12976  pcmpt  12979  pcmpt2  12980  pcbc  12987  4sqlem7  13020  4sqlem10  13023  mul4sqlem  13029  4sqlem11  13037  ennnfonelemp1  13090  setsabsd  13184  setscom  13185  ressbasd  13213  strressid  13217  ressinbasd  13220  ressressg  13221  ressplusgd  13275  prdsval  13419  pwsplusgval  13441  pwsmulrval  13442  imasival  13452  qusin  13472  fvprif  13489  xpsfeq  13491  grpidpropdg  13520  gsumpropd  13538  gsumpropd2  13539  gsumress  13541  prdssgrpd  13561  mnd32g  13573  mnd4g  13575  prdsidlem  13593  prdsmndd  13594  pws0g  13597  imasmnd2  13598  0mhm  13632  resmhm  13633  mhmco  13636  gsumwmhm  13644  grpinvcnv  13714  grpinvpropdg  13721  grpinvsub  13728  grpaddsubass  13736  grpsubpropdg  13750  grpsubpropd2  13751  prdsinvlem  13754  pwsinvg  13758  pwssub  13759  imasgrp2  13760  imasgrp  13761  qusgrp2  13763  mulgnnp1  13780  mulgnegnn  13782  mulgaddcom  13796  mulginvcom  13797  mulgnndir  13801  mulgnn0ass  13808  mhmmulg  13813  mulgpropdg  13814  submmulg  13816  subginv  13831  subgsub  13836  subgmulg  13838  eqglact  13875  ghmsub  13901  ghmmulg  13906  resghm  13910  ghmeql  13917  conjghm  13926  ablsub4  13963  ablsub32  13972  imasabl  13986  gsumfzreidx  13987  gsumfzmptfidmadd  13989  gsumfzconst  13991  mgpress  14008  rngsubdi  14028  rngsubdir  14029  imasrng  14033  dfur2g  14039  srgass  14048  srgmulgass  14066  srgpcomp  14067  srglmhm  14070  srgrmhm  14071  crngcom  14091  ringass  14093  ringcom  14108  ringsubdi  14133  ringsubdir  14134  mulgass2  14135  ringlghm  14138  ringrghm  14139  imasring  14141  opprrng  14154  opprring  14156  oppr0g  14158  oppr1g  14159  opprnegg  14160  mulgass3  14162  dvdsrvald  14171  unitlinv  14204  unitrinv  14205  dvrfvald  14211  dvrass  14217  dvrdir  14221  rdivmuldivd  14222  rngidpropdg  14224  dvdsrpropdg  14225  unitpropdg  14226  invrpropdg  14227  rhm1  14245  rhmopp  14254  subrguss  14314  subrginv  14315  subrgdv  14316  rrgsupp  14344  lmodcom  14412  lmodsubdir  14424  rmodislmod  14430  lsppropd  14511  srascag  14521  sravscag  14522  ixpsnbasval  14545  rsp0  14572  lidlrsppropdg  14574  rnglidlmsgrp  14576  gsumfzfsumlemm  14666  expghmap  14686  mulgghm2  14687  mulgrhm  14688  zlmlemg  14707  zlmsca  14711  znle  14716  psrbasg  14758  psrplusgg  14762  psrlinv  14768  tgdom  14866  txbasval  15061  cnmpt11  15077  cnmpt21  15085  setsmsbasg  15273  bdbl  15297  dvmulxxbr  15496  dvimulf  15500  dvcj  15503  dvfre  15504  dvrecap  15507  dvmptc  15511  dvmptfsum  15519  dvef  15521  plyaddlem1  15541  plyrecj  15557  dvply1  15559  sinperlem  15602  coshalfpip  15616  ptolemy  15618  tangtx  15632  relogef  15658  rpcxpadd  15699  rpmulcxp  15703  rpdivcxp  15705  cxpmul  15706  rpcxpmul2  15707  abscxp  15709  rpcxpsqrt  15716  rpabscxpbnd  15734  rplogbreexp  15747  rprelogbmul  15749  rprelogbdiv  15751  pellexlem3  15776  1sgmprm  15791  perfect1  15795  perfectlem2  15797  perfect  15798  lgsneg  15826  lgsmod  15828  lgsdir2  15835  lgsdirprm  15836  lgsdir  15837  lgsdi  15839  lgssq  15842  lgssq2  15843  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem6  15869  lgseisenlem1  15872  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlem1  15879  lgsquad2  15885  2sqlem3  15919  setsiedg  15976  vtxdeqd  16220  vtxdfifiun  16221  trlsegvdegfi  16391  depindlem3  16432  bj-charfundcALT  16508  nninfsellemeqinf  16725  refeq  16739  gfsumval  16792  gsumgfsumlem  16795