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 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  un12  4102  in12  4155  indif1  4206  difundi  4214  difundir  4215  difindi  4216  difindir  4217  dif32  4227  csbvarg  4366  undif1  4410  resmpt3  5949  xp0  6066  partfun  6589  fresaunres2  6655  caov12  7509  caov13  7511  caov411  7513  caovdir  7515  orduniss2  7689  fparlem3  7963  fparlem4  7964  fsplitfpar  7968  hartogslem1  9310  ttrclco  9485  kmlem3  9917  djuassen  9943  xpdjuen  9944  halfnq  10741  reclem3pr  10814  addcmpblnr  10834  ltsrpr  10842  pn0sr  10866  sqgt0sr  10871  map2psrpr  10875  negsubdii  11315  halfpm6th  12203  i4  13930  nn0opthlem1  13991  fac4  14004  imi  14877  bpoly3  15777  ef01bndlem  15902  bitsres  16189  gcdaddmlem  16240  modsubi  16782  gcdmodi  16784  numexpp1  16788  karatsuba  16794  oppgcntr  18981  frgpuplem  19387  0frgp  19394  ressmpladd  21239  ressmplmul  21240  ressmplvsca  21241  ltbwe  21254  ressply1add  21410  ressply1mul  21411  ressply1vsca  21412  sn0cld  22250  qtopres  22858  itg1addlem5  24874  cospi  25638  sincos4thpi  25679  sincos3rdpi  25682  dvlog  25815  dvlog2  25817  dvsqrt  25904  dvcnsqrt  25906  ang180lem3  25970  1cubrlem  26000  mcubic  26006  quart1lem  26014  atantayl2  26097  log2cnv  26103  log2ublem2  26106  log2ub  26108  gam1  26223  chtub  26369  bclbnd  26437  bposlem8  26448  lgsdir2lem1  26482  lgsdir2lem5  26486  2lgsoddprmlem3d  26570  ex-bc  28825  ex-gcd  28830  ipidsq  29081  ip1ilem  29197  ipdirilem  29200  ipasslem10  29210  siilem1  29222  hvmul2negi  29419  hvadd12i  29428  hvnegdii  29433  normlem1  29481  normlem9  29489  normsubi  29512  normpar2i  29527  polid2i  29528  chjassi  29857  chj12i  29893  pjoml2i  29956  hoadd12i  30148  lnophmlem2  30388  nmopcoadj2i  30473  indifundif  30882  aciunf1  31009  fressupp  31031  ffsrn  31073  dpmul10  31178  dpmul1000  31182  dpadd2  31193  dpadd  31194  dpmul  31196  cycpmconjslem1  31430  archirngz  31452  sqsscirc1  31867  sigaclfu2  32098  eulerpartlemd  32342  coinflippvt  32460  ballotth  32513  hgt750lem  32640  hgt750lem2  32641  quad3  33637  onint1  34647  bj-csbsn  35098  cnambfre  35834  sqmid3api  40318  re1m1e0m0  40387  sn-1ticom  40423  rabren3dioph  40644  arearect  41053  areaquad  41054  resnonrel  41207  cononrel1  41209  cononrel2  41210  lhe4.4ex1a  41954  expgrowthi  41958  expgrowth  41960  binomcxplemnotnn0  41981  liminf0  43341  dvcosre  43460  stoweidlem34  43582  fouriersw  43779