Theorem 3eqtr4d 2213

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

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  fnsnfv  5555  fvco2  5565  resfunexg  5717  fcof1  5762  fliftfun  5775  caovdir2d  6029  caov32d  6033  caov31d  6035  caov4d  6037  caovlem2d  6045  caofcom  6084  cnvf1olem  6203  tfrlem1  6287  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  frecrdg  6387  oav2  6442  omv2  6444  omsuc  6451  nnmsucr  6467  ecovicom  6621  ecoviass  6623  ecovidi  6625  nnnninfeq  7104  nninfwlpoimlemg  7151  carden2bex  7166  addcompig  7291  addasspig  7292  mulcompig  7293  mulasspig  7294  distrpig  7295  addassnqg  7344  addnq0mo  7409  mulnq0mo  7410  nqnq0a  7416  nqnq0m  7417  distrnq0  7421  mulcomnq0  7422  addassnq0  7424  addcmpblnr  7701  mulcmpblnrlemg  7702  addsrmo  7705  mulsrmo  7706  ltsrprg  7709  recexgt0sr  7735  mulgt0sr  7740  mulextsr1lem  7742  addcnsrec  7804  mulcnsrec  7805  pitonnlem2  7809  recidpirqlemcalc  7819  axaddcom  7832  adddir  7911  mul32  8049  mul31  8050  add32  8078  add4  8080  sub32  8153  sub4  8164  subdir  8305  mulneg2  8315  mulreim  8523  apadd1  8527  apneg  8530  divassap  8607  divdirap  8614  divmul13ap  8632  divmul24ap  8633  divdiv32ap  8637  conjmulap  8646  zeo  9317  xaddcom  9818  xnegdi  9825  xaddass  9826  xaddass2  9827  xpncan  9828  xadd4d  9842  lincmb01cmp  9960  iccf1o  9961  flhalf  10258  modqvalp1  10299  modqdi  10348  modqsubdir  10349  frecuzrdgg  10372  seq3shft2  10429  seq3caopr3  10437  seq3caopr  10439  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3homo  10466  seqfeq3  10468  seq3distr  10469  expp1  10483  expnegap0  10484  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  sqneg  10535  sqdivap  10540  subsq2  10583  binom2  10587  modqexp  10602  facp1  10664  bcm1k  10694  bcp1n  10695  bcval5  10697  omgadd  10737  hashun  10740  hashxp  10761  shftfibg  10784  shftfib  10787  shftval  10789  2shfti  10795  seq3shft  10802  crre  10821  remim  10824  mulreap  10828  reneg  10832  readd  10833  remullem  10835  redivap  10838  imneg  10840  imadd  10841  imdivap  10845  cjcj  10847  cjadd  10848  cjmulrcl  10851  cjneg  10854  imval2  10858  resqrexlemcalc1  10978  absneg  11014  sqabsadd  11019  sqabssub  11020  absmul  11033  absresq  11042  absexp  11043  absexpzap  11044  bdtrilem  11202  xrmaxiflemcom  11212  xrmaxadd  11224  xrminrecl  11236  xrminadd  11238  serf0  11315  summodclem3  11343  fsum3  11350  isumss  11354  fisumss  11355  fsumadd  11369  isummulc1  11390  isumdivapc  11391  fsum2dlemstep  11397  fisumcom2  11401  fisum0diag2  11410  fsummulc2  11411  fsummulc1  11412  fsumdivapc  11413  fsumconst  11417  telfsumo  11429  fsumparts  11433  binomlem  11446  isumshft  11453  arisum2  11462  geolim  11474  geo2sum  11477  geo2lim  11479  cvgratnnlemseq  11489  cvgratz  11495  mertenslem2  11499  prodfrecap  11509  prodfdivap  11510  prodmodclem2a  11539  fprodntrivap  11547  fprodssdc  11553  fprodmul  11554  fprodabs  11579  fprod2dlemstep  11585  fprodcom2fi  11589  fprodrec  11592  efcllemp  11621  efcj  11636  efexp  11645  resinval  11678  recosval  11679  cosneg  11690  efival  11695  sinadd  11699  cosadd  11700  addcos  11709  sin2t  11712  cos2t  11713  dvdsmodexp  11757  odd2np1lem  11831  oexpneg  11836  neggcd  11938  gcdabs2  11945  mulgcd  11971  mulgcdr  11973  gcddiv  11974  rplpwr  11982  eucalgval  12008  eucalginv  12010  eucalg  12013  neglcm  12029  lcmgcd  12032  mulgcddvds  12048  qredeu  12051  nn0gcdsq  12154  phimullem  12179  prmdiv  12189  coprimeprodsq  12211  pythagtriplem1  12219  pythagtriplem3  12221  pythagtriplem4  12222  pythagtriplem12  12229  pceulem  12248  pceu  12249  pcqmul  12257  pcexp  12263  pcneg  12278  pcadd  12293  pcmpt  12295  pcmpt2  12296  pcbc  12303  4sqlem7  12336  4sqlem10  12339  mul4sqlem  12345  ennnfonelemp1  12361  setsabsd  12455  setscom  12456  grpidpropdg  12628  mnd32g  12663  mnd4g  12665  0mhm  12704  mhmco  12705  grpinvcnv  12767  tgdom  12866  txbasval  13061  cnmpt11  13077  cnmpt21  13085  setsmsbasg  13273  bdbl  13297  dvmulxxbr  13460  dvimulf  13464  dvcj  13467  dvfre  13468  dvrecap  13471  dvef  13482  sinperlem  13523  coshalfpip  13537  ptolemy  13539  tangtx  13553  relogef  13579  rpcxpadd  13620  rpmulcxp  13624  rpdivcxp  13626  cxpmul  13627  abscxp  13629  rpcxpsqrt  13636  rpabscxpbnd  13653  rplogbreexp  13665  rprelogbmul  13667  rprelogbdiv  13669  lgsneg  13719  lgsmod  13721  lgsdir2  13728  lgsdirprm  13729  lgsdir  13730  lgsdi  13732  lgssq  13735  lgssq2  13736  lgsdirnn0  13742  lgsdinn0  13743  2sqlem3  13747  bj-charfundcALT  13844  nninfsellemeqinf  14049  refeq  14060