Theorem 3eqtr3i 2791

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  un12  4119  in12  4174  indif1  4228  difundi  4236  difundir  4237  difindi  4238  difindir  4239  dif32  4248  csbvarg  4392  undif1  4430  unidif0  5324  resmpt3  6034  xp0OLD  6150  partfun  6680  fresaunres2  6748  caov12  7643  caov13  7645  caov411  7647  caovdir  7649  orduniss2  7830  fparlem3  8112  fparlem4  8113  fsplitfpar  8116  hartogslem1  9517  ttrclco  9700  kmlem3  10158  djuassen  10184  xpdjuen  10185  halfnq  10988  reclem3pr  11061  addcmpblnr  11081  ltsrpr  11089  pn0sr  11113  sqgt0sr  11118  map2psrpr  11122  negsubdii  11570  8th4div3  12491  i4  14271  nn0opthlem1  14335  fac4  14348  imi  15247  bpoly3  16147  ef01bndlem  16275  bitsres  16566  gcdaddmlem  16617  modsubi  17167  gcdmodi  17169  numexpp1  17172  karatsuba  17178  oppgcntr  19495  frgpuplem  19902  0frgp  19909  pzriprnglem11  21707  ressmpladd  22247  ressmplmul  22248  ressmplvsca  22249  ltbwe  22263  ressply1add  22457  ressply1mul  22458  ressply1vsca  22459  sn0cld  23318  qtopres  23927  itg1addlem5  25931  cospi  26713  sincos4thpi  26754  sincos3rdpi  26757  dvlog  26891  dvlog2  26893  dvsqrt  26982  dvcnsqrt  26984  ang180lem3  27051  1cubrlem  27081  mcubic  27087  quart1lem  27095  atantayl2  27178  log2cnv  27184  log2ublem2  27187  log2ub  27189  gam1  27304  chtub  27451  bclbnd  27519  bposlem8  27530  lgsdir2lem1  27564  lgsdir2lem5  27568  2lgsoddprmlem3d  27652  ex-bc  30935  ex-gcd  30940  ipidsq  31194  ip1ilem  31310  ipdirilem  31313  ipasslem10  31323  siilem1  31335  hvmul2negi  31532  hvadd12i  31541  hvnegdii  31546  normlem1  31594  normlem9  31602  normsubi  31625  normpar2i  31640  polid2i  31641  chjassi  31970  chj12i  32006  pjoml2i  32069  hoadd12i  32261  lnophmlem2  32501  nmopcoadj2i  32586  indifundif  33002  ififcom  33028  aciunf1  33139  partfun2  33152  fressupp  33163  ffsrn  33202  dpmul10  33343  dpmul1000  33347  dpadd2  33358  dpadd  33359  dpmul  33361  cycpmconjslem1  33597  archirngz  33632  psrbasfsupp  34024  cos9thpiminplylem4  34298  cos9thpiminplylem5  34299  sqsscirc1  34421  sigaclfu2  34634  eulerpartlemd  34880  coinflippvt  34999  ballotth  35052  hgt750lem  35162  hgt750lem2  35163  quad3  36252  onint1  37071  bj-csbsn  37650  cnambfre  38420  vxp  39014  sqmid3api  43161  sin2t3rdpi  43231  cos2t3rdpi  43232  sin4t3rdpi  43233  cos4t3rdpi  43234  redvmptabs  43238  re1m1e0m0  43275  sn-1ticom  43313  rabren3dioph  43659  arearect  44059  areaquad  44060  resnonrel  44435  cononrel1  44437  cononrel2  44438  lhe4.4ex1a  45156  expgrowthi  45160  expgrowth  45162  binomcxplemnotnn0  45183  liminf0  46624  dvcosre  46743  stoweidlem34  46865  fouriersw  47062  goldratmolem2  47754  ceil5half3  48237  tposresg  49807  tposideq  49817  veroquadgsumlem  50819