Theorem 3eqtr4d 2281

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  fnsnfv  5762  fvco2  5774  resfunexg  5936  fcof1  5989  fliftfun  6002  caovdir2d  6266  caov32d  6270  caov31d  6272  caov4d  6274  caovlem2d  6282  f1o3d  6298  caofcom  6333  caofdig  6336  cnvf1olem  6460  tfrlem1  6579  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  frecrdg  6679  oav2  6736  omv2  6738  omsuc  6745  nnmsucr  6761  ecovicom  6917  ecoviass  6919  ecovidi  6921  nnnninfeq  7468  nninfwlpoimlemg  7515  carden2bex  7535  addcompig  7696  addasspig  7697  mulcompig  7698  mulasspig  7699  distrpig  7700  addassnqg  7749  addnq0mo  7814  mulnq0mo  7815  nqnq0a  7821  nqnq0m  7822  distrnq0  7826  mulcomnq0  7827  addassnq0  7829  addcmpblnr  8106  mulcmpblnrlemg  8107  addsrmo  8110  mulsrmo  8111  ltsrprg  8114  recexgt0sr  8140  mulgt0sr  8145  mulextsr1lem  8147  addcnsrec  8209  mulcnsrec  8210  pitonnlem2  8214  recidpirqlemcalc  8224  axaddcom  8237  adddir  8317  mul32  8456  mul31  8457  add32  8485  add4  8487  sub32  8560  sub4  8571  subdir  8713  mulneg2  8723  mulreim  8932  apadd1  8936  apneg  8939  divassap  9020  divdirap  9027  divmul13ap  9045  divmul24ap  9046  divdiv32ap  9050  conjmulap  9059  zeo  9751  xaddcom  10263  xnegdi  10270  xaddass  10271  xaddass2  10272  xpncan  10273  xadd4d  10287  lincmb01cmp  10405  iccf1o  10407  flhalf  10737  modqvalp1  10780  modqdi  10829  modqsubdir  10830  frecuzrdgg  10853  seq3shft2  10918  seqshft2g  10919  seq3caopr3  10928  seqcaopr3g  10929  seq3caopr  10932  seqcaoprg  10933  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  seqf1oglem2a  10955  seqf1oglem2  10957  seqf1og  10958  seq3homo  10964  seqfeq3  10966  seqhomog  10967  seqfeq4g  10968  seq3distr  10969  expp1  10983  expnegap0  10984  expaddzaplem  11019  expaddzap  11020  expmulzap  11022  sqneg  11035  sqdivap  11040  subsq2  11084  binom2  11088  modqexp  11104  facp1  11168  bcm1k  11198  bcp1n  11199  bcval5  11201  omgadd  11242  hashun  11245  hashxp  11267  hashfibclem  11282  hashf1  11287  csbwrdg  11334  ccatass  11376  lswccatn0lsw  11379  swrdlsw  11441  swrdswrd  11477  wrd2ind  11495  swrdccatin1  11497  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccatpfx1  11508  swrdccat3blem  11511  cats1catd  11540  shftfibg  11585  shftfib  11588  shftval  11590  2shfti  11596  seq3shft  11603  crre  11622  remim  11625  mulreap  11629  reneg  11633  readd  11634  remullem  11636  redivap  11639  imneg  11641  imadd  11642  imdivap  11646  cjcj  11648  cjadd  11649  cjmulrcl  11652  cjneg  11655  imval2  11659  resqrexlemcalc1  11780  absneg  11816  sqabsadd  11821  sqabssub  11822  absmul  11835  absresq  11844  absexp  11845  absexpzap  11846  bdtrilem  12005  xrmaxiflemcom  12015  xrmaxadd  12027  xrminrecl  12039  xrminadd  12041  serf0  12118  summodclem3  12147  fsum3  12154  isumss  12158  fisumss  12159  fsumadd  12173  isummulc1  12194  isumdivapc  12195  fsum2dlemstep  12201  fisumcom2  12205  fisum0diag2  12214  fsummulc2  12215  fsummulc1  12216  fsumdivapc  12217  fsumconst  12221  telfsumo  12233  fsumparts  12237  binomlem  12250  isumshft  12257  arisum2  12266  geolim  12278  geo2sum  12281  geo2lim  12283  cvgratnnlemseq  12293  cvgratz  12299  mertenslem2  12303  prodfrecap  12313  prodfdivap  12314  prodmodclem2a  12343  fprodntrivap  12351  fprodssdc  12357  fprodmul  12358  fprodabs  12383  fprod2dlemstep  12389  fprodcom2fi  12393  fprodrec  12396  efcllemp  12425  efcj  12440  efexp  12449  resinval  12482  recosval  12483  cosneg  12494  efival  12499  sinadd  12503  cosadd  12504  addcos  12513  sin2t  12516  cos2t  12517  dvdsmodexp  12562  odd2np1lem  12639  oexpneg  12644  neggcd  12760  gcdabs2  12767  mulgcd  12793  mulgcdr  12795  gcddiv  12796  rplpwr  12804  eucalgval  12832  eucalginv  12834  eucalg  12837  neglcm  12853  lcmgcd  12856  mulgcddvds  12872  qredeu  12875  nn0gcdsq  12978  phimullem  13003  prmdiv  13013  coprimeprodsq  13036  pythagtriplem1  13044  pythagtriplem3  13046  pythagtriplem4  13047  pythagtriplem12  13054  pceulem  13073  pceu  13074  pcqmul  13082  pcexp  13088  pcneg  13104  pcadd  13119  pcmpt  13122  pcmpt2  13123  pcbc  13130  4sqlem7  13163  4sqlem10  13166  mul4sqlem  13172  4sqlem11  13180  ballotfilemfp1  13231  ballotfilemieq  13260  ballotfilemgun  13268  ballotfilemfrc  13270  ennnfonelemp1  13297  setsabsd  13391  setscom  13392  ressbasd  13421  strressid  13425  ressinbasd  13428  ressressg  13429  ressplusgd  13483  imasival  13627  qusin  13647  fvprif  13664  xpsfeq  13666  grpidpropdg  13694  gzsumress  13712  mnd32g  13740  mnd4g  13742  imasmnd2  13759  0mhm  13793  resmhm  13794  mhmco  13797  gzsumwmhm  13803  grpinvcnv  13873  grpinvpropdg  13880  grpinvsub  13887  grpaddsubass  13895  grpsubpropdg  13909  grpsubpropd2  13910  imasgrp2  13913  imasgrp  13914  qusgrp2  13916  mulgnnp1  13933  mulgnegnn  13935  mulgaddcom  13949  mulginvcom  13950  mulgnndir  13954  mulgnn0ass  13961  mhmmulg  13966  mulgpropdg  13967  submmulg  13969  subginv  13984  subgsub  13989  subgmulg  13991  eqglact  14028  ghmsub  14054  ghmmulg  14059  resghm  14063  ghmeql  14070  conjghm  14079  ablsub4  14117  ablsub32  14126  imasabl  14140  gzsumreidx  14141  gzsumconst  14143  gzsumshift  14149  gsumvalfi  14152  gsumf1ofi  14160  gsummptfidmadd  14161  gsummhmfi  14164  gsumconstcmn  14166  gsumressfi  14167  prdsval  14173  prdssgrpd  14191  prdsidlem  14193  prdsmndd  14194  prdsinvlem  14196  pwsplusgval  14208  pwsmulrval  14209  pws0g  14213  pwsinvg  14215  pwssub  14216  mgpress  14230  rngsubdi  14250  rngsubdir  14251  imasrng  14255  dfur2g  14266  srgass  14275  srgmulgass  14293  srgpcomp  14294  srglmhm  14297  srgrmhm  14298  crngcom  14318  ringass  14320  ringcom  14336  ringsubdi  14361  ringsubdir  14362  mulgass2  14363  ringlghm  14366  ringrghm  14367  imasring  14369  opprrng  14382  opprring  14384  oppr0g  14387  oppr1g  14388  opprnegg  14389  mulgass3  14391  dvdsrvald  14400  unitlinv  14433  unitrinv  14434  dvrfvald  14440  dvrass  14446  dvrdir  14450  rdivmuldivd  14451  rngidpropdg  14453  dvdsrpropdg  14454  unitpropdg  14455  invrpropdg  14456  rhm1  14474  rhmopp  14483  subrguss  14544  subrginv  14545  subrgdv  14546  rrgsupp  14574  aprprop  14601  opprdrng  14620  lmodcom  14670  lmodsubdir  14682  rmodislmod  14688  lsppropd  14769  srascag  14779  sravscag  14780  ixpsnbasval  14803  rsp0  14830  lidlrsppropdg  14832  rnglidlmsgrp  14834  gsumfsum  14923  expghmap  14942  mulgghm2  14943  mulgrhm  14944  zlmlemg  14963  zlmsca  14967  znle  14972  asclghm  15025  ascldimul  15031  assamulgscmlem1  15041  psrbasg  15065  psrplusgg  15069  psrlinv  15075  tgdom  15173  txbasval  15368  cnmpt11  15384  cnmpt21  15392  setsmsbasg  15580  bdbl  15604  dvmulxxbr  15803  dvimulf  15807  dvcj  15810  dvfre  15811  dvrecap  15814  dvmptc  15818  dvmptfsum  15826  dvef  15828  plyaddlem1  15848  plyrecj  15864  dvply1  15866  sinperlem  15909  coshalfpip  15923  ptolemy  15925  tangtx  15939  relogef  15965  logfac  15995  rpcxpadd  16007  rpmulcxp  16011  rpdivcxp  16013  cxpmul  16014  rpcxpmul2  16015  abscxp  16017  rpcxpsqrt  16024  rpabscxpbnd  16042  rplogbreexp  16055  rprelogbmul  16057  rprelogbdiv  16059  birthdaylem2  16088  pellexlem3  16093  1sgmprm  16108  perfect1  16112  perfectlem2  16114  perfect  16115  lgsneg  16143  lgsmod  16145  lgsdir2  16152  lgsdirprm  16153  lgsdir  16154  lgsdi  16156  lgssq  16159  lgssq2  16160  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem6  16186  lgseisenlem1  16189  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlem1  16196  lgsquad2  16202  2sqlem3  16236  setsiedg  16293  vtxdeqd  16537  vtxdfifiun  16538  trlsegvdegfi  16708  depindlem3  16749  bj-charfundcALT  16835  nninfsellemeqinf  17059  refeq  17073