Theorem 3eqtr3i 2775

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 2769	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2769	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731

This theorem is referenced by:  un12  4105  in12  4159  indif1  4210  difundi  4218  difundir  4219  difindi  4220  difindir  4221  dif32  4231  csbvarg  4370  undif1  4414  resmpt3  5943  xp0  6058  partfun  6576  fresaunres2  6642  caov12  7491  caov13  7493  caov411  7495  caovdir  7497  orduniss2  7668  fparlem3  7938  fparlem4  7939  fsplitfpar  7943  hartogslem1  9262  ttrclco  9437  kmlem3  9892  djuassen  9918  xpdjuen  9919  halfnq  10716  reclem3pr  10789  addcmpblnr  10809  ltsrpr  10817  pn0sr  10841  sqgt0sr  10846  map2psrpr  10850  negsubdii  11289  halfpm6th  12177  i4  13902  nn0opthlem1  13963  fac4  13976  imi  14849  bpoly3  15749  ef01bndlem  15874  bitsres  16161  gcdaddmlem  16212  modsubi  16754  gcdmodi  16756  numexpp1  16760  karatsuba  16766  oppgcntr  18953  frgpuplem  19359  0frgp  19366  ressmpladd  21211  ressmplmul  21212  ressmplvsca  21213  ltbwe  21226  ressply1add  21382  ressply1mul  21383  ressply1vsca  21384  sn0cld  22222  qtopres  22830  itg1addlem5  24846  cospi  25610  sincos4thpi  25651  sincos3rdpi  25654  dvlog  25787  dvlog2  25789  dvsqrt  25876  dvcnsqrt  25878  ang180lem3  25942  1cubrlem  25972  mcubic  25978  quart1lem  25986  atantayl2  26069  log2cnv  26075  log2ublem2  26078  log2ub  26080  gam1  26195  chtub  26341  bclbnd  26409  bposlem8  26420  lgsdir2lem1  26454  lgsdir2lem5  26458  2lgsoddprmlem3d  26542  ex-bc  28795  ex-gcd  28800  ipidsq  29051  ip1ilem  29167  ipdirilem  29170  ipasslem10  29180  siilem1  29192  hvmul2negi  29389  hvadd12i  29398  hvnegdii  29403  normlem1  29451  normlem9  29459  normsubi  29482  normpar2i  29497  polid2i  29498  chjassi  29827  chj12i  29863  pjoml2i  29926  hoadd12i  30118  lnophmlem2  30358  nmopcoadj2i  30443  indifundif  30852  aciunf1  30979  fressupp  31001  ffsrn  31043  dpmul10  31148  dpmul1000  31152  dpadd2  31163  dpadd  31164  dpmul  31166  cycpmconjslem1  31400  archirngz  31422  sqsscirc1  31837  sigaclfu2  32068  eulerpartlemd  32312  coinflippvt  32430  ballotth  32483  hgt750lem  32610  hgt750lem2  32611  quad3  33607  onint1  34617  bj-csbsn  35068  cnambfre  35804  sqmid3api  40291  re1m1e0m0  40360  sn-1ticom  40396  rabren3dioph  40617  arearect  41026  areaquad  41027  resnonrel  41153  cononrel1  41155  cononrel2  41156  lhe4.4ex1a  41900  expgrowthi  41904  expgrowth  41906  binomcxplemnotnn0  41927  liminf0  43288  dvcosre  43407  stoweidlem34  43529  fouriersw  43726