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  4114  in12  4170  indif1  4223  difundi  4231  difundir  4232  difindi  4233  difindir  4234  dif32  4243  csbvarg  4375  undif1  4417  unidif0  5298  resmpt3  5999  xp0OLD  6118  partfun  6641  fresaunres2  6708  caov12  7590  caov13  7592  caov411  7594  caovdir  7596  orduniss2  7779  fparlem3  8059  fparlem4  8060  fsplitfpar  8063  hartogslem1  9452  ttrclco  9634  kmlem3  10070  djuassen  10096  xpdjuen  10097  halfnq  10894  reclem3pr  10967  addcmpblnr  10987  ltsrpr  10995  pn0sr  11019  sqgt0sr  11024  map2psrpr  11028  negsubdii  11474  i4  14161  nn0opthlem1  14225  fac4  14238  imi  15114  bpoly3  16018  ef01bndlem  16146  bitsres  16437  gcdaddmlem  16488  modsubi  17038  gcdmodi  17040  numexpp1  17043  karatsuba  17049  oppgcntr  19335  frgpuplem  19742  0frgp  19749  pzriprnglem11  21485  ressmpladd  22021  ressmplmul  22022  ressmplvsca  22023  ltbwe  22036  ressply1add  22207  ressply1mul  22208  ressply1vsca  22209  sn0cld  23069  qtopres  23677  itg1addlem5  25681  cospi  26453  sincos4thpi  26494  sincos3rdpi  26498  dvlog  26632  dvlog2  26634  dvsqrt  26723  dvcnsqrt  26725  ang180lem3  26792  1cubrlem  26822  mcubic  26828  quart1lem  26836  atantayl2  26919  log2cnv  26925  log2ublem2  26928  log2ub  26930  gam1  27046  chtub  27193  bclbnd  27261  bposlem8  27272  lgsdir2lem1  27306  lgsdir2lem5  27310  2lgsoddprmlem3d  27394  ex-bc  30541  ex-gcd  30546  ipidsq  30800  ip1ilem  30916  ipdirilem  30919  ipasslem10  30929  siilem1  30941  hvmul2negi  31138  hvadd12i  31147  hvnegdii  31152  normlem1  31200  normlem9  31208  normsubi  31231  normpar2i  31246  polid2i  31247  chjassi  31576  chj12i  31612  pjoml2i  31675  hoadd12i  31867  lnophmlem2  32107  nmopcoadj2i  32192  indifundif  32613  aciunf1  32755  partfun2  32768  fressupp  32780  ffsrn  32820  dpmul10  32973  dpmul1000  32977  dpadd2  32988  dpadd  32989  dpmul  32991  cycpmconjslem1  33234  archirngz  33269  psrbasfsupp  33691  cos9thpiminplylem4  33949  cos9thpiminplylem5  33950  sqsscirc1  34072  sigaclfu2  34285  eulerpartlemd  34530  coinflippvt  34649  ballotth  34702  hgt750lem  34815  hgt750lem2  34816  quad3  35872  onint1  36651  bj-csbsn  37231  cnambfre  38007  vxp  38602  sqmid3api  42733  sin2t3rdpi  42803  cos2t3rdpi  42804  sin4t3rdpi  42805  cos4t3rdpi  42806  redvmptabs  42810  re1m1e0m0  42847  sn-1ticom  42885  rabren3dioph  43265  arearect  43665  areaquad  43666  resnonrel  44041  cononrel1  44043  cononrel2  44044  lhe4.4ex1a  44778  expgrowthi  44782  expgrowth  44784  binomcxplemnotnn0  44805  liminf0  46243  dvcosre  46362  stoweidlem34  46484  fouriersw  46681  ceil5half3  47810  tposresg  49369  tposideq  49379