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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  fnsnfv  5705  fvco2  5715  resfunexg  5875  fcof1  5924  fliftfun  5937  caovdir2d  6199  caov32d  6203  caov31d  6205  caov4d  6207  caovlem2d  6215  caofcom  6266  caofdig  6269  cnvf1olem  6389  tfrlem1  6474  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  frecrdg  6574  oav2  6631  omv2  6633  omsuc  6640  nnmsucr  6656  ecovicom  6812  ecoviass  6814  ecovidi  6816  nnnninfeq  7327  nninfwlpoimlemg  7374  carden2bex  7394  addcompig  7549  addasspig  7550  mulcompig  7551  mulasspig  7552  distrpig  7553  addassnqg  7602  addnq0mo  7667  mulnq0mo  7668  nqnq0a  7674  nqnq0m  7675  distrnq0  7679  mulcomnq0  7680  addassnq0  7682  addcmpblnr  7959  mulcmpblnrlemg  7960  addsrmo  7963  mulsrmo  7964  ltsrprg  7967  recexgt0sr  7993  mulgt0sr  7998  mulextsr1lem  8000  addcnsrec  8062  mulcnsrec  8063  pitonnlem2  8067  recidpirqlemcalc  8077  axaddcom  8090  adddir  8170  mul32  8309  mul31  8310  add32  8338  add4  8340  sub32  8413  sub4  8424  subdir  8565  mulneg2  8575  mulreim  8784  apadd1  8788  apneg  8791  divassap  8870  divdirap  8877  divmul13ap  8895  divmul24ap  8896  divdiv32ap  8900  conjmulap  8909  zeo  9585  xaddcom  10096  xnegdi  10103  xaddass  10104  xaddass2  10105  xpncan  10106  xadd4d  10120  lincmb01cmp  10238  iccf1o  10239  flhalf  10563  modqvalp1  10606  modqdi  10655  modqsubdir  10656  frecuzrdgg  10679  seq3shft2  10744  seqshft2g  10745  seq3caopr3  10754  seqcaopr3g  10755  seq3caopr  10758  seqcaoprg  10759  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seqf1oglem2a  10781  seqf1oglem2  10783  seqf1og  10784  seq3homo  10790  seqfeq3  10792  seqhomog  10793  seqfeq4g  10794  seq3distr  10795  expp1  10809  expnegap0  10810  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  sqneg  10861  sqdivap  10866  subsq2  10910  binom2  10914  modqexp  10929  facp1  10993  bcm1k  11023  bcp1n  11024  bcval5  11026  omgadd  11066  hashun  11069  hashxp  11091  csbwrdg  11147  ccatass  11189  lswccatn0lsw  11192  swrdlsw  11254  swrdswrd  11290  wrd2ind  11308  swrdccatin1  11310  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatpfx1  11321  swrdccat3blem  11324  cats1catd  11353  shftfibg  11398  shftfib  11401  shftval  11403  2shfti  11409  seq3shft  11416  crre  11435  remim  11438  mulreap  11442  reneg  11446  readd  11447  remullem  11449  redivap  11452  imneg  11454  imadd  11455  imdivap  11459  cjcj  11461  cjadd  11462  cjmulrcl  11465  cjneg  11468  imval2  11472  resqrexlemcalc1  11592  absneg  11628  sqabsadd  11633  sqabssub  11634  absmul  11647  absresq  11656  absexp  11657  absexpzap  11658  bdtrilem  11817  xrmaxiflemcom  11827  xrmaxadd  11839  xrminrecl  11851  xrminadd  11853  serf0  11930  summodclem3  11959  fsum3  11966  isumss  11970  fisumss  11971  fsumadd  11985  isummulc1  12006  isumdivapc  12007  fsum2dlemstep  12013  fisumcom2  12017  fisum0diag2  12026  fsummulc2  12027  fsummulc1  12028  fsumdivapc  12029  fsumconst  12033  telfsumo  12045  fsumparts  12049  binomlem  12062  isumshft  12069  arisum2  12078  geolim  12090  geo2sum  12093  geo2lim  12095  cvgratnnlemseq  12105  cvgratz  12111  mertenslem2  12115  prodfrecap  12125  prodfdivap  12126  prodmodclem2a  12155  fprodntrivap  12163  fprodssdc  12169  fprodmul  12170  fprodabs  12195  fprod2dlemstep  12201  fprodcom2fi  12205  fprodrec  12208  efcllemp  12237  efcj  12252  efexp  12261  resinval  12294  recosval  12295  cosneg  12306  efival  12311  sinadd  12315  cosadd  12316  addcos  12325  sin2t  12328  cos2t  12329  dvdsmodexp  12374  odd2np1lem  12451  oexpneg  12456  neggcd  12572  gcdabs2  12579  mulgcd  12605  mulgcdr  12607  gcddiv  12608  rplpwr  12616  eucalgval  12644  eucalginv  12646  eucalg  12649  neglcm  12665  lcmgcd  12668  mulgcddvds  12684  qredeu  12687  nn0gcdsq  12790  phimullem  12815  prmdiv  12825  coprimeprodsq  12848  pythagtriplem1  12856  pythagtriplem3  12858  pythagtriplem4  12859  pythagtriplem12  12866  pceulem  12885  pceu  12886  pcqmul  12894  pcexp  12900  pcneg  12916  pcadd  12931  pcmpt  12934  pcmpt2  12935  pcbc  12942  4sqlem7  12975  4sqlem10  12978  mul4sqlem  12984  4sqlem11  12992  ennnfonelemp1  13045  setsabsd  13139  setscom  13140  ressbasd  13168  strressid  13172  ressinbasd  13175  ressressg  13176  ressplusgd  13230  prdsval  13374  pwsplusgval  13396  pwsmulrval  13397  imasival  13407  qusin  13427  fvprif  13444  xpsfeq  13446  grpidpropdg  13475  gsumpropd  13493  gsumpropd2  13494  gsumress  13496  prdssgrpd  13516  mnd32g  13528  mnd4g  13530  prdsidlem  13548  prdsmndd  13549  pws0g  13552  imasmnd2  13553  0mhm  13587  resmhm  13588  mhmco  13591  gsumwmhm  13599  grpinvcnv  13669  grpinvpropdg  13676  grpinvsub  13683  grpaddsubass  13691  grpsubpropdg  13705  grpsubpropd2  13706  prdsinvlem  13709  pwsinvg  13713  pwssub  13714  imasgrp2  13715  imasgrp  13716  qusgrp2  13718  mulgnnp1  13735  mulgnegnn  13737  mulgaddcom  13751  mulginvcom  13752  mulgnndir  13756  mulgnn0ass  13763  mhmmulg  13768  mulgpropdg  13769  submmulg  13771  subginv  13786  subgsub  13791  subgmulg  13793  eqglact  13830  ghmsub  13856  ghmmulg  13861  resghm  13865  ghmeql  13872  conjghm  13881  ablsub4  13918  ablsub32  13927  imasabl  13941  gsumfzreidx  13942  gsumfzmptfidmadd  13944  gsumfzconst  13946  mgpress  13963  rngsubdi  13983  rngsubdir  13984  imasrng  13988  dfur2g  13994  srgass  14003  srgmulgass  14021  srgpcomp  14022  srglmhm  14025  srgrmhm  14026  crngcom  14046  ringass  14048  ringcom  14063  ringsubdi  14088  ringsubdir  14089  mulgass2  14090  ringlghm  14093  ringrghm  14094  imasring  14096  opprrng  14109  opprring  14111  oppr0g  14113  oppr1g  14114  opprnegg  14115  mulgass3  14117  dvdsrvald  14126  unitlinv  14159  unitrinv  14160  dvrfvald  14166  dvrass  14172  dvrdir  14176  rdivmuldivd  14177  rngidpropdg  14179  dvdsrpropdg  14180  unitpropdg  14181  invrpropdg  14182  rhm1  14200  rhmopp  14209  subrguss  14269  subrginv  14270  subrgdv  14271  lmodcom  14366  lmodsubdir  14378  rmodislmod  14384  lsppropd  14465  srascag  14475  sravscag  14476  ixpsnbasval  14499  rsp0  14526  lidlrsppropdg  14528  rnglidlmsgrp  14530  gsumfzfsumlemm  14620  expghmap  14640  mulgghm2  14641  mulgrhm  14642  zlmlemg  14661  zlmsca  14665  znle  14670  psrbasg  14707  psrplusgg  14711  psrlinv  14717  tgdom  14815  txbasval  15010  cnmpt11  15026  cnmpt21  15034  setsmsbasg  15222  bdbl  15246  dvmulxxbr  15445  dvimulf  15449  dvcj  15452  dvfre  15453  dvrecap  15456  dvmptc  15460  dvmptfsum  15468  dvef  15470  plyaddlem1  15490  plyrecj  15506  dvply1  15508  sinperlem  15551  coshalfpip  15565  ptolemy  15567  tangtx  15581  relogef  15607  rpcxpadd  15648  rpmulcxp  15652  rpdivcxp  15654  cxpmul  15655  rpcxpmul2  15656  abscxp  15658  rpcxpsqrt  15665  rpabscxpbnd  15683  rplogbreexp  15696  rprelogbmul  15698  rprelogbdiv  15700  1sgmprm  15737  perfect1  15741  perfectlem2  15743  perfect  15744  lgsneg  15772  lgsmod  15774  lgsdir2  15781  lgsdirprm  15782  lgsdir  15783  lgsdi  15785  lgssq  15788  lgssq2  15789  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem6  15815  lgseisenlem1  15818  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlem1  15825  lgsquad2  15831  2sqlem3  15865  setsiedg  15922  vtxdeqd  16166  vtxdfifiun  16167  trlsegvdegfi  16337  depindlem3  16378  bj-charfundcALT  16455  nninfsellemeqinf  16669  refeq  16683  gfsumval  16732  gsumgfsumlem  16735