Theorem 3eqtr4d 2239

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  fnsnfv  5620  fvco2  5630  resfunexg  5783  fcof1  5830  fliftfun  5843  caovdir2d  6100  caov32d  6104  caov31d  6106  caov4d  6108  caovlem2d  6116  caofcom  6161  caofdig  6164  cnvf1olem  6282  tfrlem1  6366  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  frecrdg  6466  oav2  6521  omv2  6523  omsuc  6530  nnmsucr  6546  ecovicom  6702  ecoviass  6704  ecovidi  6706  nnnninfeq  7194  nninfwlpoimlemg  7241  carden2bex  7256  addcompig  7396  addasspig  7397  mulcompig  7398  mulasspig  7399  distrpig  7400  addassnqg  7449  addnq0mo  7514  mulnq0mo  7515  nqnq0a  7521  nqnq0m  7522  distrnq0  7526  mulcomnq0  7527  addassnq0  7529  addcmpblnr  7806  mulcmpblnrlemg  7807  addsrmo  7810  mulsrmo  7811  ltsrprg  7814  recexgt0sr  7840  mulgt0sr  7845  mulextsr1lem  7847  addcnsrec  7909  mulcnsrec  7910  pitonnlem2  7914  recidpirqlemcalc  7924  axaddcom  7937  adddir  8017  mul32  8156  mul31  8157  add32  8185  add4  8187  sub32  8260  sub4  8271  subdir  8412  mulneg2  8422  mulreim  8631  apadd1  8635  apneg  8638  divassap  8717  divdirap  8724  divmul13ap  8742  divmul24ap  8743  divdiv32ap  8747  conjmulap  8756  zeo  9431  xaddcom  9936  xnegdi  9943  xaddass  9944  xaddass2  9945  xpncan  9946  xadd4d  9960  lincmb01cmp  10078  iccf1o  10079  flhalf  10392  modqvalp1  10435  modqdi  10484  modqsubdir  10485  frecuzrdgg  10508  seq3shft2  10573  seqshft2g  10574  seq3caopr3  10583  seqcaopr3g  10584  seq3caopr  10587  seqcaoprg  10588  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seqf1oglem2a  10610  seqf1oglem2  10612  seqf1og  10613  seq3homo  10619  seqfeq3  10621  seqhomog  10622  seqfeq4g  10623  seq3distr  10624  expp1  10638  expnegap0  10639  expaddzaplem  10674  expaddzap  10675  expmulzap  10677  sqneg  10690  sqdivap  10695  subsq2  10739  binom2  10743  modqexp  10758  facp1  10822  bcm1k  10852  bcp1n  10853  bcval5  10855  omgadd  10894  hashun  10897  hashxp  10918  csbwrdg  10964  shftfibg  10985  shftfib  10988  shftval  10990  2shfti  10996  seq3shft  11003  crre  11022  remim  11025  mulreap  11029  reneg  11033  readd  11034  remullem  11036  redivap  11039  imneg  11041  imadd  11042  imdivap  11046  cjcj  11048  cjadd  11049  cjmulrcl  11052  cjneg  11055  imval2  11059  resqrexlemcalc1  11179  absneg  11215  sqabsadd  11220  sqabssub  11221  absmul  11234  absresq  11243  absexp  11244  absexpzap  11245  bdtrilem  11404  xrmaxiflemcom  11414  xrmaxadd  11426  xrminrecl  11438  xrminadd  11440  serf0  11517  summodclem3  11545  fsum3  11552  isumss  11556  fisumss  11557  fsumadd  11571  isummulc1  11592  isumdivapc  11593  fsum2dlemstep  11599  fisumcom2  11603  fisum0diag2  11612  fsummulc2  11613  fsummulc1  11614  fsumdivapc  11615  fsumconst  11619  telfsumo  11631  fsumparts  11635  binomlem  11648  isumshft  11655  arisum2  11664  geolim  11676  geo2sum  11679  geo2lim  11681  cvgratnnlemseq  11691  cvgratz  11697  mertenslem2  11701  prodfrecap  11711  prodfdivap  11712  prodmodclem2a  11741  fprodntrivap  11749  fprodssdc  11755  fprodmul  11756  fprodabs  11781  fprod2dlemstep  11787  fprodcom2fi  11791  fprodrec  11794  efcllemp  11823  efcj  11838  efexp  11847  resinval  11880  recosval  11881  cosneg  11892  efival  11897  sinadd  11901  cosadd  11902  addcos  11911  sin2t  11914  cos2t  11915  dvdsmodexp  11960  odd2np1lem  12037  oexpneg  12042  neggcd  12150  gcdabs2  12157  mulgcd  12183  mulgcdr  12185  gcddiv  12186  rplpwr  12194  eucalgval  12222  eucalginv  12224  eucalg  12227  neglcm  12243  lcmgcd  12246  mulgcddvds  12262  qredeu  12265  nn0gcdsq  12368  phimullem  12393  prmdiv  12403  coprimeprodsq  12426  pythagtriplem1  12434  pythagtriplem3  12436  pythagtriplem4  12437  pythagtriplem12  12444  pceulem  12463  pceu  12464  pcqmul  12472  pcexp  12478  pcneg  12494  pcadd  12509  pcmpt  12512  pcmpt2  12513  pcbc  12520  4sqlem7  12553  4sqlem10  12556  mul4sqlem  12562  4sqlem11  12570  ennnfonelemp1  12623  setsabsd  12717  setscom  12718  ressbasd  12745  strressid  12749  ressinbasd  12752  ressressg  12753  ressplusgd  12806  imasival  12949  qusin  12969  fvprif  12986  xpsfeq  12988  grpidpropdg  13017  gsumpropd  13035  gsumpropd2  13036  gsumress  13038  mnd32g  13068  mnd4g  13070  0mhm  13118  resmhm  13119  mhmco  13122  gsumwmhm  13130  grpinvcnv  13200  grpinvpropdg  13207  grpinvsub  13214  grpaddsubass  13222  grpsubpropdg  13236  grpsubpropd2  13237  imasgrp2  13240  imasgrp  13241  qusgrp2  13243  mulgnnp1  13260  mulgnegnn  13262  mulgaddcom  13276  mulginvcom  13277  mulgnndir  13281  mulgnn0ass  13288  mhmmulg  13293  mulgpropdg  13294  submmulg  13296  subginv  13311  subgsub  13316  subgmulg  13318  eqglact  13355  ghmsub  13381  ghmmulg  13386  resghm  13390  ghmeql  13397  conjghm  13406  ablsub4  13443  ablsub32  13452  imasabl  13466  gsumfzreidx  13467  gsumfzmptfidmadd  13469  gsumfzconst  13471  mgpress  13487  rngsubdi  13507  rngsubdir  13508  imasrng  13512  dfur2g  13518  srgass  13527  srgmulgass  13545  srgpcomp  13546  srglmhm  13549  srgrmhm  13550  crngcom  13570  ringass  13572  ringcom  13587  ringsubdi  13612  ringsubdir  13613  mulgass2  13614  ringlghm  13617  ringrghm  13618  imasring  13620  opprrng  13633  opprring  13635  oppr0g  13637  oppr1g  13638  opprnegg  13639  mulgass3  13641  dvdsrvald  13649  unitlinv  13682  unitrinv  13683  dvrfvald  13689  dvrass  13695  dvrdir  13699  rdivmuldivd  13700  rngidpropdg  13702  dvdsrpropdg  13703  unitpropdg  13704  invrpropdg  13705  rhm1  13723  rhmopp  13732  subrguss  13792  subrginv  13793  subrgdv  13794  lmodcom  13889  lmodsubdir  13901  rmodislmod  13907  lsppropd  13988  srascag  13998  sravscag  13999  ixpsnbasval  14022  rsp0  14049  lidlrsppropdg  14051  rnglidlmsgrp  14053  gsumfzfsumlemm  14143  expghmap  14163  mulgghm2  14164  mulgrhm  14165  zlmlemg  14184  zlmsca  14188  znle  14193  psrbasg  14227  psrplusgg  14230  tgdom  14308  txbasval  14503  cnmpt11  14519  cnmpt21  14527  setsmsbasg  14715  bdbl  14739  dvmulxxbr  14938  dvimulf  14942  dvcj  14945  dvfre  14946  dvrecap  14949  dvmptc  14953  dvmptfsum  14961  dvef  14963  plyaddlem1  14983  plyrecj  14999  dvply1  15001  sinperlem  15044  coshalfpip  15058  ptolemy  15060  tangtx  15074  relogef  15100  rpcxpadd  15141  rpmulcxp  15145  rpdivcxp  15147  cxpmul  15148  rpcxpmul2  15149  abscxp  15151  rpcxpsqrt  15158  rpabscxpbnd  15176  rplogbreexp  15189  rprelogbmul  15191  rprelogbdiv  15193  1sgmprm  15230  perfect1  15234  perfectlem2  15236  perfect  15237  lgsneg  15265  lgsmod  15267  lgsdir2  15274  lgsdirprm  15275  lgsdir  15276  lgsdi  15278  lgssq  15281  lgssq2  15282  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem6  15308  lgseisenlem1  15311  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlem1  15318  lgsquad2  15324  2sqlem3  15358  bj-charfundcALT  15455  nninfsellemeqinf  15660  refeq  15672