Theorem 3eqtr3i 2774

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  un12  4097  in12  4151  indif1  4202  difundi  4210  difundir  4211  difindi  4212  difindir  4213  dif32  4223  csbvarg  4362  undif1  4406  resmpt3  5935  xp0  6050  partfun  6564  fresaunres2  6630  caov12  7478  caov13  7480  caov411  7482  caovdir  7484  orduniss2  7655  fparlem3  7925  fparlem4  7926  fsplitfpar  7930  hartogslem1  9231  kmlem3  9839  djuassen  9865  xpdjuen  9866  halfnq  10663  reclem3pr  10736  addcmpblnr  10756  ltsrpr  10764  pn0sr  10788  sqgt0sr  10793  map2psrpr  10797  negsubdii  11236  halfpm6th  12124  i4  13849  nn0opthlem1  13910  fac4  13923  imi  14796  bpoly3  15696  ef01bndlem  15821  bitsres  16108  gcdaddmlem  16159  modsubi  16701  gcdmodi  16703  numexpp1  16707  karatsuba  16713  oppgcntr  18887  frgpuplem  19293  0frgp  19300  ressmpladd  21140  ressmplmul  21141  ressmplvsca  21142  ltbwe  21155  ressply1add  21311  ressply1mul  21312  ressply1vsca  21313  sn0cld  22149  qtopres  22757  itg1addlem5  24770  cospi  25534  sincos4thpi  25575  sincos3rdpi  25578  dvlog  25711  dvlog2  25713  dvsqrt  25800  dvcnsqrt  25802  ang180lem3  25866  1cubrlem  25896  mcubic  25902  quart1lem  25910  atantayl2  25993  log2cnv  25999  log2ublem2  26002  log2ub  26004  gam1  26119  chtub  26265  bclbnd  26333  bposlem8  26344  lgsdir2lem1  26378  lgsdir2lem5  26382  2lgsoddprmlem3d  26466  ex-bc  28717  ex-gcd  28722  ipidsq  28973  ip1ilem  29089  ipdirilem  29092  ipasslem10  29102  siilem1  29114  hvmul2negi  29311  hvadd12i  29320  hvnegdii  29325  normlem1  29373  normlem9  29381  normsubi  29404  normpar2i  29419  polid2i  29420  chjassi  29749  chj12i  29785  pjoml2i  29848  hoadd12i  30040  lnophmlem2  30280  nmopcoadj2i  30365  indifundif  30774  aciunf1  30902  fressupp  30924  ffsrn  30966  dpmul10  31071  dpmul1000  31075  dpadd2  31086  dpadd  31087  dpmul  31089  cycpmconjslem1  31323  archirngz  31345  sqsscirc1  31760  sigaclfu2  31989  eulerpartlemd  32233  coinflippvt  32351  ballotth  32404  hgt750lem  32531  hgt750lem2  32532  quad3  33528  ttrclco  33704  onint1  34565  bj-csbsn  35016  cnambfre  35752  sqmid3api  40232  re1m1e0m0  40301  sn-1ticom  40337  rabren3dioph  40553  arearect  40962  areaquad  40963  resnonrel  41089  cononrel1  41091  cononrel2  41092  lhe4.4ex1a  41836  expgrowthi  41840  expgrowth  41842  binomcxplemnotnn0  41863  liminf0  43224  dvcosre  43343  stoweidlem34  43465  fouriersw  43662