Theorem 3eqtr3i 2768

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 2762	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2762	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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  un12  4167  in12  4220  indif1  4271  difundi  4279  difundir  4280  difindi  4281  difindir  4282  dif32  4292  csbvarg  4431  undif1  4475  resmpt3  6038  xp0  6157  partfun  6697  fresaunres2  6763  caov12  7634  caov13  7636  caov411  7638  caovdir  7640  orduniss2  7820  fparlem3  8099  fparlem4  8100  fsplitfpar  8103  hartogslem1  9536  ttrclco  9712  kmlem3  10146  djuassen  10172  xpdjuen  10173  halfnq  10970  reclem3pr  11043  addcmpblnr  11063  ltsrpr  11071  pn0sr  11095  sqgt0sr  11100  map2psrpr  11104  negsubdii  11544  halfpm6th  12432  i4  14167  nn0opthlem1  14227  fac4  14240  imi  15103  bpoly3  16001  ef01bndlem  16126  bitsres  16413  gcdaddmlem  16464  modsubi  17004  gcdmodi  17006  numexpp1  17010  karatsuba  17016  oppgcntr  19231  frgpuplem  19639  0frgp  19646  ressmpladd  21583  ressmplmul  21584  ressmplvsca  21585  ltbwe  21598  ressply1add  21751  ressply1mul  21752  ressply1vsca  21753  sn0cld  22593  qtopres  23201  itg1addlem5  25217  cospi  25981  sincos4thpi  26022  sincos3rdpi  26025  dvlog  26158  dvlog2  26160  dvsqrt  26247  dvcnsqrt  26249  ang180lem3  26313  1cubrlem  26343  mcubic  26349  quart1lem  26357  atantayl2  26440  log2cnv  26446  log2ublem2  26449  log2ub  26451  gam1  26566  chtub  26712  bclbnd  26780  bposlem8  26791  lgsdir2lem1  26825  lgsdir2lem5  26829  2lgsoddprmlem3d  26913  ex-bc  29702  ex-gcd  29707  ipidsq  29958  ip1ilem  30074  ipdirilem  30077  ipasslem10  30087  siilem1  30099  hvmul2negi  30296  hvadd12i  30305  hvnegdii  30310  normlem1  30358  normlem9  30366  normsubi  30389  normpar2i  30404  polid2i  30405  chjassi  30734  chj12i  30770  pjoml2i  30833  hoadd12i  31025  lnophmlem2  31265  nmopcoadj2i  31350  indifundif  31757  aciunf1  31883  fressupp  31905  ffsrn  31949  dpmul10  32056  dpmul1000  32060  dpadd2  32071  dpadd  32072  dpmul  32074  cycpmconjslem1  32308  archirngz  32330  sqsscirc1  32883  sigaclfu2  33114  eulerpartlemd  33360  coinflippvt  33478  ballotth  33531  hgt750lem  33658  hgt750lem2  33659  quad3  34650  onint1  35329  bj-csbsn  35779  cnambfre  36531  sqmid3api  41197  re1m1e0m0  41271  sn-1ticom  41308  rabren3dioph  41543  arearect  41954  areaquad  41955  resnonrel  42333  cononrel1  42335  cononrel2  42336  lhe4.4ex1a  43078  expgrowthi  43082  expgrowth  43084  binomcxplemnotnn0  43105  liminf0  44499  dvcosre  44618  stoweidlem34  44740  fouriersw  44937  pzriprnglem11  46805