Theorem 3eqtr3i 2772

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

Syntax hints:   = wceq 1548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733

This theorem is referenced by:  un12  4105  in12  4160  indif1  4213  difundi  4221  difundir  4222  difindi  4223  difindir  4224  dif32  4233  csbvarg  4365  undif1  4407  unidif0  5291  resmpt3  5997  xp0OLD  6113  partfun  6636  fresaunres2  6703  caov12  7588  caov13  7590  caov411  7592  caovdir  7594  orduniss2  7777  fparlem3  8057  fparlem4  8058  fsplitfpar  8061  hartogslem1  9451  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  21470  ressmpladd  22008  ressmplmul  22009  ressmplvsca  22010  ltbwe  22024  ressply1add  22218  ressply1mul  22219  ressply1vsca  22220  sn0cld  23077  qtopres  23685  itg1addlem5  25689  cospi  26458  sincos4thpi  26499  sincos3rdpi  26503  dvlog  26637  dvlog2  26639  dvsqrt  26728  dvcnsqrt  26730  ang180lem3  26797  1cubrlem  26827  mcubic  26833  quart1lem  26841  atantayl2  26924  log2cnv  26930  log2ublem2  26933  log2ub  26935  gam1  27050  chtub  27197  bclbnd  27265  bposlem8  27276  lgsdir2lem1  27310  lgsdir2lem5  27314  2lgsoddprmlem3d  27398  ex-bc  30544  ex-gcd  30549  ipidsq  30803  ip1ilem  30919  ipdirilem  30922  ipasslem10  30932  siilem1  30944  hvmul2negi  31141  hvadd12i  31150  hvnegdii  31155  normlem1  31203  normlem9  31211  normsubi  31234  normpar2i  31249  polid2i  31250  chjassi  31579  chj12i  31615  pjoml2i  31678  hoadd12i  31870  lnophmlem2  32110  nmopcoadj2i  32195  indifundif  32616  ififcom  32642  aciunf1  32759  partfun2  32772  fressupp  32784  ffsrn  32824  dpmul10  32977  dpmul1000  32981  dpadd2  32992  dpadd  32993  dpmul  32995  cycpmconjslem1  33239  archirngz  33274  psrbasfsupp  33707  cos9thpiminplylem4  33981  cos9thpiminplylem5  33982  sqsscirc1  34104  sigaclfu2  34317  eulerpartlemd  34562  coinflippvt  34681  ballotth  34734  hgt750lem  34847  hgt750lem2  34848  quad3  35913  onint1  36692  bj-csbsn  37272  cnambfre  38050  vxp  38645  sqmid3api  42775  sin2t3rdpi  42845  cos2t3rdpi  42846  sin4t3rdpi  42847  cos4t3rdpi  42848  redvmptabs  42852  re1m1e0m0  42889  sn-1ticom  42927  rabren3dioph  43275  arearect  43675  areaquad  43676  resnonrel  44051  cononrel1  44053  cononrel2  44054  lhe4.4ex1a  44788  expgrowthi  44792  expgrowth  44794  binomcxplemnotnn0  44815  liminf0  46250  dvcosre  46369  stoweidlem34  46491  fouriersw  46688  goldratmolem2  47363  ceil5half3  47823  tposresg  49382  tposideq  49392