Theorem 3eqtr3i 2765

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 2759	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2759	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 2123  ax-ext 2706

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

This theorem is referenced by:  un12  4123  in12  4179  indif1  4232  difundi  4240  difundir  4241  difindi  4242  difindir  4243  dif32  4252  csbvarg  4384  undif1  4426  resmpt3  5995  xp0OLD  6114  partfun  6637  fresaunres2  6704  caov12  7584  caov13  7586  caov411  7588  caovdir  7590  orduniss2  7773  fparlem3  8054  fparlem4  8055  fsplitfpar  8058  hartogslem1  9445  ttrclco  9625  kmlem3  10061  djuassen  10087  xpdjuen  10088  halfnq  10885  reclem3pr  10958  addcmpblnr  10978  ltsrpr  10986  pn0sr  11010  sqgt0sr  11015  map2psrpr  11019  negsubdii  11464  i4  14125  nn0opthlem1  14189  fac4  14202  imi  15078  bpoly3  15979  ef01bndlem  16107  bitsres  16398  gcdaddmlem  16449  modsubi  16998  gcdmodi  17000  numexpp1  17003  karatsuba  17009  oppgcntr  19292  frgpuplem  19699  0frgp  19706  pzriprnglem11  21444  ressmpladd  21982  ressmplmul  21983  ressmplvsca  21984  ltbwe  21997  ressply1add  22168  ressply1mul  22169  ressply1vsca  22170  sn0cld  23032  qtopres  23640  itg1addlem5  25655  cospi  26435  sincos4thpi  26476  sincos3rdpi  26480  dvlog  26614  dvlog2  26616  dvsqrt  26705  dvcnsqrt  26707  ang180lem3  26775  1cubrlem  26805  mcubic  26811  quart1lem  26819  atantayl2  26902  log2cnv  26908  log2ublem2  26911  log2ub  26913  gam1  27029  chtub  27177  bclbnd  27245  bposlem8  27256  lgsdir2lem1  27290  lgsdir2lem5  27294  2lgsoddprmlem3d  27378  ex-bc  30476  ex-gcd  30481  ipidsq  30734  ip1ilem  30850  ipdirilem  30853  ipasslem10  30863  siilem1  30875  hvmul2negi  31072  hvadd12i  31081  hvnegdii  31086  normlem1  31134  normlem9  31142  normsubi  31165  normpar2i  31180  polid2i  31181  chjassi  31510  chj12i  31546  pjoml2i  31609  hoadd12i  31801  lnophmlem2  32041  nmopcoadj2i  32126  indifundif  32548  aciunf1  32690  partfun2  32704  fressupp  32716  ffsrn  32756  dpmul10  32925  dpmul1000  32929  dpadd2  32940  dpadd  32941  dpmul  32943  cycpmconjslem1  33185  archirngz  33220  psrbasfsupp  33642  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  sqsscirc1  34014  sigaclfu2  34227  eulerpartlemd  34472  coinflippvt  34591  ballotth  34644  hgt750lem  34757  hgt750lem2  34758  quad3  35813  onint1  36592  bj-csbsn  37048  cnambfre  37808  sqmid3api  42480  sin2t3rdpi  42550  cos2t3rdpi  42551  sin4t3rdpi  42552  cos4t3rdpi  42553  redvmptabs  42557  re1m1e0m0  42594  sn-1ticom  42632  rabren3dioph  42999  arearect  43399  areaquad  43400  resnonrel  43775  cononrel1  43777  cononrel2  43778  lhe4.4ex1a  44512  expgrowthi  44516  expgrowth  44518  binomcxplemnotnn0  44539  liminf0  45979  dvcosre  46098  stoweidlem34  46220  fouriersw  46417  ceil5half3  47528  tposresg  49065  tposideq  49075