Theorem 3eqtr3i 2760

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 2754	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2754	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  un12  4132  in12  4188  indif1  4241  difundi  4249  difundir  4250  difindi  4251  difindir  4252  dif32  4261  csbvarg  4393  undif1  4435  resmpt3  5998  xp0  6119  partfun  6647  fresaunres2  6714  caov12  7597  caov13  7599  caov411  7601  caovdir  7603  orduniss2  7788  fparlem3  8070  fparlem4  8071  fsplitfpar  8074  hartogslem1  9471  ttrclco  9647  kmlem3  10082  djuassen  10108  xpdjuen  10109  halfnq  10905  reclem3pr  10978  addcmpblnr  10998  ltsrpr  11006  pn0sr  11030  sqgt0sr  11035  map2psrpr  11039  negsubdii  11483  i4  14145  nn0opthlem1  14209  fac4  14222  imi  15099  bpoly3  16000  ef01bndlem  16128  bitsres  16419  gcdaddmlem  16470  modsubi  17019  gcdmodi  17021  numexpp1  17024  karatsuba  17030  oppgcntr  19279  frgpuplem  19686  0frgp  19693  pzriprnglem11  21433  ressmpladd  21969  ressmplmul  21970  ressmplvsca  21971  ltbwe  21984  ressply1add  22147  ressply1mul  22148  ressply1vsca  22149  sn0cld  23010  qtopres  23618  itg1addlem5  25634  cospi  26414  sincos4thpi  26455  sincos3rdpi  26459  dvlog  26593  dvlog2  26595  dvsqrt  26684  dvcnsqrt  26686  ang180lem3  26754  1cubrlem  26784  mcubic  26790  quart1lem  26798  atantayl2  26881  log2cnv  26887  log2ublem2  26890  log2ub  26892  gam1  27008  chtub  27156  bclbnd  27224  bposlem8  27235  lgsdir2lem1  27269  lgsdir2lem5  27273  2lgsoddprmlem3d  27357  ex-bc  30431  ex-gcd  30436  ipidsq  30689  ip1ilem  30805  ipdirilem  30808  ipasslem10  30818  siilem1  30830  hvmul2negi  31027  hvadd12i  31036  hvnegdii  31041  normlem1  31089  normlem9  31097  normsubi  31120  normpar2i  31135  polid2i  31136  chjassi  31465  chj12i  31501  pjoml2i  31564  hoadd12i  31756  lnophmlem2  31996  nmopcoadj2i  32081  indifundif  32503  aciunf1  32637  fressupp  32661  ffsrn  32702  dpmul10  32865  dpmul1000  32869  dpadd2  32880  dpadd  32881  dpmul  32883  cycpmconjslem1  33126  archirngz  33158  cos9thpiminplylem4  33768  cos9thpiminplylem5  33769  sqsscirc1  33891  sigaclfu2  34104  eulerpartlemd  34350  coinflippvt  34469  ballotth  34522  hgt750lem  34635  hgt750lem2  34636  quad3  35650  onint1  36430  bj-csbsn  36885  cnambfre  37655  sqmid3api  42264  sin2t3rdpi  42334  cos2t3rdpi  42335  sin4t3rdpi  42336  cos4t3rdpi  42337  redvmptabs  42341  re1m1e0m0  42378  sn-1ticom  42416  rabren3dioph  42796  arearect  43197  areaquad  43198  resnonrel  43574  cononrel1  43576  cononrel2  43577  lhe4.4ex1a  44311  expgrowthi  44315  expgrowth  44317  binomcxplemnotnn0  44338  liminf0  45784  dvcosre  45903  stoweidlem34  46025  fouriersw  46222  ceil5half3  47334  tposresg  48859  tposideq  48869