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 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  un12  4127  in12  4183  indif1  4236  difundi  4244  difundir  4245  difindi  4246  difindir  4247  dif32  4256  csbvarg  4388  undif1  4430  resmpt3  6007  xp0OLD  6126  partfun  6649  fresaunres2  6716  caov12  7598  caov13  7600  caov411  7602  caovdir  7604  orduniss2  7787  fparlem3  8068  fparlem4  8069  fsplitfpar  8072  hartogslem1  9461  ttrclco  9641  kmlem3  10077  djuassen  10103  xpdjuen  10104  halfnq  10901  reclem3pr  10974  addcmpblnr  10994  ltsrpr  11002  pn0sr  11026  sqgt0sr  11031  map2psrpr  11035  negsubdii  11480  i4  14141  nn0opthlem1  14205  fac4  14218  imi  15094  bpoly3  15995  ef01bndlem  16123  bitsres  16414  gcdaddmlem  16465  modsubi  17014  gcdmodi  17016  numexpp1  17019  karatsuba  17025  oppgcntr  19311  frgpuplem  19718  0frgp  19725  pzriprnglem11  21463  ressmpladd  22001  ressmplmul  22002  ressmplvsca  22003  ltbwe  22016  ressply1add  22187  ressply1mul  22188  ressply1vsca  22189  sn0cld  23051  qtopres  23659  itg1addlem5  25674  cospi  26454  sincos4thpi  26495  sincos3rdpi  26499  dvlog  26633  dvlog2  26635  dvsqrt  26724  dvcnsqrt  26726  ang180lem3  26794  1cubrlem  26824  mcubic  26830  quart1lem  26838  atantayl2  26921  log2cnv  26927  log2ublem2  26930  log2ub  26932  gam1  27048  chtub  27196  bclbnd  27264  bposlem8  27275  lgsdir2lem1  27309  lgsdir2lem5  27313  2lgsoddprmlem3d  27397  ex-bc  30545  ex-gcd  30550  ipidsq  30804  ip1ilem  30920  ipdirilem  30923  ipasslem10  30933  siilem1  30945  hvmul2negi  31142  hvadd12i  31151  hvnegdii  31156  normlem1  31204  normlem9  31212  normsubi  31235  normpar2i  31250  polid2i  31251  chjassi  31580  chj12i  31616  pjoml2i  31679  hoadd12i  31871  lnophmlem2  32111  nmopcoadj2i  32196  indifundif  32617  aciunf1  32759  partfun2  32772  fressupp  32784  ffsrn  32824  dpmul10  32993  dpmul1000  32997  dpadd2  33008  dpadd  33009  dpmul  33011  cycpmconjslem1  33254  archirngz  33289  psrbasfsupp  33711  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  sqsscirc1  34092  sigaclfu2  34305  eulerpartlemd  34550  coinflippvt  34669  ballotth  34722  hgt750lem  34835  hgt750lem2  34836  quad3  35892  onint1  36671  bj-csbsn  37179  cnambfre  37948  vxp  38543  sqmid3api  42682  sin2t3rdpi  42752  cos2t3rdpi  42753  sin4t3rdpi  42754  cos4t3rdpi  42755  redvmptabs  42759  re1m1e0m0  42796  sn-1ticom  42834  rabren3dioph  43201  arearect  43601  areaquad  43602  resnonrel  43977  cononrel1  43979  cononrel2  43980  lhe4.4ex1a  44714  expgrowthi  44718  expgrowth  44720  binomcxplemnotnn0  44741  liminf0  46180  dvcosre  46299  stoweidlem34  46421  fouriersw  46618  ceil5half3  47729  tposresg  49266  tposideq  49276