Theorem 3eqtr3i 2762

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 2756	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2756	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  un12  4120  in12  4176  indif1  4229  difundi  4237  difundir  4238  difindi  4239  difindir  4240  dif32  4249  csbvarg  4381  undif1  4423  resmpt3  5986  xp0OLD  6105  partfun  6628  fresaunres2  6695  caov12  7574  caov13  7576  caov411  7578  caovdir  7580  orduniss2  7763  fparlem3  8044  fparlem4  8045  fsplitfpar  8048  hartogslem1  9428  ttrclco  9608  kmlem3  10044  djuassen  10070  xpdjuen  10071  halfnq  10867  reclem3pr  10940  addcmpblnr  10960  ltsrpr  10968  pn0sr  10992  sqgt0sr  10997  map2psrpr  11001  negsubdii  11446  i4  14111  nn0opthlem1  14175  fac4  14188  imi  15064  bpoly3  15965  ef01bndlem  16093  bitsres  16384  gcdaddmlem  16435  modsubi  16984  gcdmodi  16986  numexpp1  16989  karatsuba  16995  oppgcntr  19277  frgpuplem  19684  0frgp  19691  pzriprnglem11  21428  ressmpladd  21964  ressmplmul  21965  ressmplvsca  21966  ltbwe  21979  ressply1add  22142  ressply1mul  22143  ressply1vsca  22144  sn0cld  23005  qtopres  23613  itg1addlem5  25628  cospi  26408  sincos4thpi  26449  sincos3rdpi  26453  dvlog  26587  dvlog2  26589  dvsqrt  26678  dvcnsqrt  26680  ang180lem3  26748  1cubrlem  26778  mcubic  26784  quart1lem  26792  atantayl2  26875  log2cnv  26881  log2ublem2  26884  log2ub  26886  gam1  27002  chtub  27150  bclbnd  27218  bposlem8  27229  lgsdir2lem1  27263  lgsdir2lem5  27267  2lgsoddprmlem3d  27351  ex-bc  30432  ex-gcd  30437  ipidsq  30690  ip1ilem  30806  ipdirilem  30809  ipasslem10  30819  siilem1  30831  hvmul2negi  31028  hvadd12i  31037  hvnegdii  31042  normlem1  31090  normlem9  31098  normsubi  31121  normpar2i  31136  polid2i  31137  chjassi  31466  chj12i  31502  pjoml2i  31565  hoadd12i  31757  lnophmlem2  31997  nmopcoadj2i  32082  indifundif  32504  aciunf1  32645  fressupp  32669  ffsrn  32711  dpmul10  32875  dpmul1000  32879  dpadd2  32890  dpadd  32891  dpmul  32893  cycpmconjslem1  33123  archirngz  33158  psrbasfsupp  33572  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  sqsscirc1  33921  sigaclfu2  34134  eulerpartlemd  34379  coinflippvt  34498  ballotth  34551  hgt750lem  34664  hgt750lem2  34665  quad3  35714  onint1  36493  bj-csbsn  36948  cnambfre  37718  sqmid3api  42386  sin2t3rdpi  42456  cos2t3rdpi  42457  sin4t3rdpi  42458  cos4t3rdpi  42459  redvmptabs  42463  re1m1e0m0  42500  sn-1ticom  42538  rabren3dioph  42918  arearect  43318  areaquad  43319  resnonrel  43695  cononrel1  43697  cononrel2  43698  lhe4.4ex1a  44432  expgrowthi  44436  expgrowth  44438  binomcxplemnotnn0  44459  liminf0  45901  dvcosre  46020  stoweidlem34  46142  fouriersw  46339  ceil5half3  47450  tposresg  48988  tposideq  48998