Theorem 3eqtr4d 2142

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

Syntax hints:   → wi 4   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093

This theorem is referenced by:  fnsnfv  5412  fvco2  5422  resfunexg  5573  fcof1  5616  fliftfun  5629  caovdir2d  5879  caov32d  5883  caov31d  5885  caov4d  5887  caovlem2d  5895  caofcom  5936  cnvf1olem  6051  tfrlem1  6135  tfrlemisucaccv  6152  tfr1onlemsucaccv  6168  tfrcllemsucaccv  6181  frecrdg  6235  oav2  6289  omv2  6291  omsuc  6298  nnmsucr  6314  ecovicom  6467  ecoviass  6469  ecovidi  6471  carden2bex  6956  addcompig  7038  addasspig  7039  mulcompig  7040  mulasspig  7041  distrpig  7042  addassnqg  7091  addnq0mo  7156  mulnq0mo  7157  nqnq0a  7163  nqnq0m  7164  distrnq0  7168  mulcomnq0  7169  addassnq0  7171  addcmpblnr  7435  mulcmpblnrlemg  7436  addsrmo  7439  mulsrmo  7440  ltsrprg  7443  recexgt0sr  7469  mulgt0sr  7473  mulextsr1lem  7475  addcnsrec  7529  mulcnsrec  7530  pitonnlem2  7534  recidpirqlemcalc  7544  axaddcom  7555  adddir  7629  mul32  7763  mul31  7764  add32  7792  add4  7794  sub32  7867  sub4  7878  subdir  8015  mulneg2  8025  mulreim  8232  apadd1  8236  apneg  8239  divassap  8311  divdirap  8318  divmul13ap  8336  divmul24ap  8337  divdiv32ap  8341  conjmulap  8350  zeo  9008  xaddcom  9485  xnegdi  9492  xaddass  9493  xaddass2  9494  xpncan  9495  xadd4d  9509  lincmb01cmp  9627  iccf1o  9628  flhalf  9916  modqvalp1  9957  modqdi  10006  modqsubdir  10007  frecuzrdgg  10030  seq3shft2  10087  seq3caopr3  10095  seq3caopr  10097  seq3f1olemqsumkj  10112  seq3f1olemqsumk  10113  seq3f1olemqsum  10114  seq3homo  10124  seqfeq3  10126  seq3distr  10127  expp1  10141  expnegap0  10142  expaddzaplem  10177  expaddzap  10178  expmulzap  10180  sqneg  10193  sqdivap  10198  subsq2  10241  binom2  10244  facp1  10317  bcm1k  10347  bcp1n  10348  bcval5  10350  omgadd  10389  hashun  10392  hashxp  10413  shftfibg  10433  shftfib  10436  shftval  10438  2shfti  10444  seq3shft  10451  crre  10470  remim  10473  mulreap  10477  reneg  10481  readd  10482  remullem  10484  redivap  10487  imneg  10489  imadd  10490  imdivap  10494  cjcj  10496  cjadd  10497  cjmulrcl  10500  cjneg  10503  imval2  10507  resqrexlemcalc1  10626  absneg  10662  sqabsadd  10667  sqabssub  10668  absmul  10681  absresq  10690  absexp  10691  absexpzap  10692  bdtrilem  10849  xrmaxiflemcom  10857  xrmaxadd  10869  xrminrecl  10881  xrminadd  10883  serf0  10960  summodclem3  10988  fsum3  10995  isumss  10999  fisumss  11000  fsumadd  11014  isummulc1  11035  isumdivapc  11036  fsum2dlemstep  11042  fisumcom2  11046  fisum0diag2  11055  fsummulc2  11056  fsummulc1  11057  fsumdivapc  11058  fsumconst  11062  telfsumo  11074  fsumparts  11078  binomlem  11091  isumshft  11098  arisum2  11107  geolim  11119  geo2sum  11122  geo2lim  11124  cvgratnnlemseq  11134  cvgratz  11140  mertenslem2  11144  efcllemp  11162  efcj  11177  efexp  11186  resinval  11220  recosval  11221  cosneg  11232  efival  11237  sinadd  11241  cosadd  11242  addcos  11251  sin2t  11254  cos2t  11255  odd2np1lem  11364  oexpneg  11369  neggcd  11466  gcdabs2  11473  mulgcd  11497  mulgcdr  11499  gcddiv  11500  rplpwr  11508  eucalgval  11528  eucalginv  11530  eucalg  11533  neglcm  11549  lcmgcd  11552  mulgcddvds  11568  qredeu  11571  nn0gcdsq  11670  phimullem  11693  ennnfonelemp1  11711  setsabsd  11780  setscom  11781  tgdom  12023  txbasval  12217  cnmpt11  12233  cnmpt21  12241  setsmsbasg  12407  bdbl  12431  nninfalllemn  12786  nninfsellemeqinf  12796  refeq  12807