Theorem 3eqtr3i 2767

Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr3i.1	⊢ 𝐴 = 𝐵
3eqtr3i.2	⊢ 𝐴 = 𝐶
3eqtr3i.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr3i

Step	Hyp	Ref	Expression
1		3eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr3i.2	. . 3 ⊢ 𝐴 = 𝐶
3	1, 2	eqtr3i 2761	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2761	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  un12  4113  in12  4169  indif1  4222  difundi  4230  difundir  4231  difindi  4232  difindir  4233  dif32  4242  csbvarg  4374  undif1  4416  unidif0  5301  resmpt3  6003  xp0OLD  6122  partfun  6645  fresaunres2  6712  caov12  7595  caov13  7597  caov411  7599  caovdir  7601  orduniss2  7784  fparlem3  8064  fparlem4  8065  fsplitfpar  8068  hartogslem1  9457  ttrclco  9639  kmlem3  10075  djuassen  10101  xpdjuen  10102  halfnq  10899  reclem3pr  10972  addcmpblnr  10992  ltsrpr  11000  pn0sr  11024  sqgt0sr  11029  map2psrpr  11033  negsubdii  11479  i4  14166  nn0opthlem1  14230  fac4  14243  imi  15119  bpoly3  16023  ef01bndlem  16151  bitsres  16442  gcdaddmlem  16493  modsubi  17043  gcdmodi  17045  numexpp1  17048  karatsuba  17054  oppgcntr  19340  frgpuplem  19747  0frgp  19754  pzriprnglem11  21471  ressmpladd  22007  ressmplmul  22008  ressmplvsca  22009  ltbwe  22022  ressply1add  22193  ressply1mul  22194  ressply1vsca  22195  sn0cld  23055  qtopres  23663  itg1addlem5  25667  cospi  26436  sincos4thpi  26477  sincos3rdpi  26481  dvlog  26615  dvlog2  26617  dvsqrt  26706  dvcnsqrt  26708  ang180lem3  26775  1cubrlem  26805  mcubic  26811  quart1lem  26819  atantayl2  26902  log2cnv  26908  log2ublem2  26911  log2ub  26913  gam1  27028  chtub  27175  bclbnd  27243  bposlem8  27254  lgsdir2lem1  27288  lgsdir2lem5  27292  2lgsoddprmlem3d  27376  ex-bc  30522  ex-gcd  30527  ipidsq  30781  ip1ilem  30897  ipdirilem  30900  ipasslem10  30910  siilem1  30922  hvmul2negi  31119  hvadd12i  31128  hvnegdii  31133  normlem1  31181  normlem9  31189  normsubi  31212  normpar2i  31227  polid2i  31228  chjassi  31557  chj12i  31593  pjoml2i  31656  hoadd12i  31848  lnophmlem2  32088  nmopcoadj2i  32173  indifundif  32594  aciunf1  32736  partfun2  32749  fressupp  32761  ffsrn  32801  dpmul10  32954  dpmul1000  32958  dpadd2  32969  dpadd  32970  dpmul  32972  cycpmconjslem1  33215  archirngz  33250  psrbasfsupp  33672  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  sqsscirc1  34052  sigaclfu2  34265  eulerpartlemd  34510  coinflippvt  34629  ballotth  34682  hgt750lem  34795  hgt750lem2  34796  quad3  35852  onint1  36631  bj-csbsn  37211  cnambfre  37989  vxp  38584  sqmid3api  42715  sin2t3rdpi  42785  cos2t3rdpi  42786  sin4t3rdpi  42787  cos4t3rdpi  42788  redvmptabs  42792  re1m1e0m0  42829  sn-1ticom  42867  rabren3dioph  43243  arearect  43643  areaquad  43644  resnonrel  44019  cononrel1  44021  cononrel2  44022  lhe4.4ex1a  44756  expgrowthi  44760  expgrowth  44762  binomcxplemnotnn0  44783  liminf0  46221  dvcosre  46340  stoweidlem34  46462  fouriersw  46659  goldratmolem2  47334  ceil5half3  47794  tposresg  49353  tposideq  49363