Theorem 3eqtr3i 2800

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  un12  4134  in12  4189  indif1  4243  difundi  4251  difundir  4252  difindi  4253  difindir  4254  dif32  4263  csbvarg  4405  undif1  4442  unidif0  5331  resmpt3  6041  xp0OLD  6156  partfun  6683  fresaunres2  6751  caov12  7639  caov13  7641  caov411  7643  caovdir  7645  orduniss2  7829  fparlem3  8109  fparlem4  8110  fsplitfpar  8113  hartogslem1  9504  ttrclco  9687  kmlem3  10136  djuassen  10162  xpdjuen  10163  halfnq  10961  reclem3pr  11034  addcmpblnr  11054  ltsrpr  11062  pn0sr  11086  sqgt0sr  11091  map2psrpr  11095  negsubdii  11543  i4  14240  nn0opthlem1  14304  fac4  14317  imi  15208  bpoly3  16112  ef01bndlem  16240  bitsres  16531  gcdaddmlem  16582  modsubi  17132  gcdmodi  17134  numexpp1  17137  karatsuba  17143  oppgcntr  19435  frgpuplem  19842  0frgp  19849  pzriprnglem11  21610  ressmpladd  22148  ressmplmul  22149  ressmplvsca  22150  ltbwe  22164  ressply1add  22358  ressply1mul  22359  ressply1vsca  22360  sn0cld  23216  qtopres  23824  itg1addlem5  25828  cospi  26603  sincos4thpi  26644  sincos3rdpi  26648  dvlog  26782  dvlog2  26784  dvsqrt  26873  dvcnsqrt  26875  ang180lem3  26942  1cubrlem  26972  mcubic  26978  quart1lem  26986  atantayl2  27069  log2cnv  27075  log2ublem2  27078  log2ub  27080  gam1  27195  chtub  27342  bclbnd  27410  bposlem8  27421  lgsdir2lem1  27455  lgsdir2lem5  27459  2lgsoddprmlem3d  27543  ex-bc  30744  ex-gcd  30749  ipidsq  31003  ip1ilem  31119  ipdirilem  31122  ipasslem10  31132  siilem1  31144  hvmul2negi  31341  hvadd12i  31350  hvnegdii  31355  normlem1  31403  normlem9  31411  normsubi  31434  normpar2i  31449  polid2i  31450  chjassi  31779  chj12i  31815  pjoml2i  31878  hoadd12i  32070  lnophmlem2  32310  nmopcoadj2i  32395  indifundif  32811  ififcom  32837  aciunf1  32949  partfun2  32962  fressupp  32974  ffsrn  33014  dpmul10  33155  dpmul1000  33159  dpadd2  33170  dpadd  33171  dpmul  33173  cycpmconjslem1  33415  archirngz  33450  psrbasfsupp  33846  cos9thpiminplylem4  34120  cos9thpiminplylem5  34121  sqsscirc1  34243  sigaclfu2  34456  eulerpartlemd  34701  coinflippvt  34820  ballotth  34873  hgt750lem  34983  hgt750lem2  34984  quad3  36095  onint1  36883  bj-csbsn  37462  cnambfre  38241  vxp  38836  sqmid3api  42968  sin2t3rdpi  43038  cos2t3rdpi  43039  sin4t3rdpi  43040  cos4t3rdpi  43041  redvmptabs  43045  re1m1e0m0  43082  sn-1ticom  43120  rabren3dioph  43468  arearect  43868  areaquad  43869  resnonrel  44244  cononrel1  44246  cononrel2  44247  lhe4.4ex1a  44965  expgrowthi  44969  expgrowth  44971  binomcxplemnotnn0  44992  liminf0  46433  dvcosre  46552  stoweidlem34  46674  fouriersw  46871  goldratmolem2  47546  ceil5half3  48006  tposresg  49575  tposideq  49585