Theorem 3eqtr3i 2792

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  un12  4119  in12  4174  indif1  4228  difundi  4236  difundir  4237  difindi  4238  difindir  4239  dif32  4248  csbvarg  4392  undif1  4430  unidif0  5321  resmpt3  6030  xp0OLD  6149  partfun  6686  fresaunres2  6754  caov12  7649  caov13  7651  caov411  7653  caovdir  7655  orduniss2  7844  fparlem3  8125  fparlem4  8126  fsplitfpar  8129  hartogslem1  9536  ttrclco  9719  kmlem3  10231  djuassen  10257  xpdjuen  10258  halfnq  11061  reclem3pr  11134  addcmpblnr  11154  ltsrpr  11162  pn0sr  11186  sqgt0sr  11191  map2psrpr  11195  negsubdii  11643  8th4div3  12566  i4  14348  nn0opthlem1  14412  fac4  14425  imi  15324  bpoly3  16224  ef01bndlem  16352  bitsres  16643  gcdaddmlem  16696  modsubi  17250  gcdmodi  17252  numexpp1  17255  karatsuba  17261  oppgcntr  19579  frgpuplem  19986  0frgp  19993  pzriprnglem11  21797  ressmpladd  22337  ressmplmul  22338  ressmplvsca  22339  ltbwe  22353  ressply1add  22547  ressply1mul  22548  ressply1vsca  22549  sn0cld  23408  qtopres  24017  itg1addlem5  26021  cospi  26801  sincos4thpi  26842  sincos3rdpi  26845  dvlog  26979  dvlog2  26981  dvsqrt  27070  dvcnsqrt  27072  ang180lem3  27139  1cubrlem  27169  mcubic  27175  quart1lem  27183  atantayl2  27266  log2cnv  27272  log2ublem2  27275  log2ub  27277  gam1  27392  chtub  27539  bclbnd  27607  bposlem8  27618  lgsdir2lem1  27652  lgsdir2lem5  27656  2lgsoddprmlem3d  27740  ex-bc  31053  ex-gcd  31058  ipidsq  31312  ip1ilem  31428  ipdirilem  31431  ipasslem10  31441  siilem1  31453  hvmul2negi  31650  hvadd12i  31659  hvnegdii  31664  normlem1  31712  normlem9  31720  normsubi  31743  normpar2i  31758  polid2i  31759  chjassi  32088  chj12i  32124  pjoml2i  32187  hoadd12i  32379  lnophmlem2  32619  nmopcoadj2i  32704  indifundif  33120  ififcom  33146  aciunf1  33257  partfun2  33270  fressupp  33281  ffsrn  33320  dpmul10  33461  dpmul1000  33465  dpadd2  33476  dpadd  33477  dpmul  33479  cycpmconjslem1  33715  archirngz  33750  psrbasfsupp  34143  cos9thpiminplylem4  34417  cos9thpiminplylem5  34418  sqsscirc1  34540  sigaclfu2  34753  eulerpartlemd  34998  coinflippvt  35117  ballotth  35170  hgt750lem  35280  hgt750lem2  35281  quad3  36435  onint1  37237  bj-csbsn  37816  cnambfre  38586  vxp  39195  sqmid3api  43340  sin2t3rdpi  43404  cos2t3rdpi  43405  sin4t3rdpi  43406  cos4t3rdpi  43407  redvmptabs  43411  re1m1e0m0  43448  sn-1ticom  43486  rabren3dioph  43821  arearect  44216  areaquad  44217  resnonrel  44591  cononrel1  44593  cononrel2  44594  lhe4.4ex1a  45312  expgrowthi  45316  expgrowth  45318  binomcxplemnotnn0  45339  liminf0  46802  dvcosre  46921  stoweidlem34  47043  fouriersw  47240  goldratmolem2  47932  ceil5half3  48415  tposresg  49985  tposideq  49995  veroquadgsumlem  50982