Theorem 3eqtr2i 2758

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2i.1	⊢ 𝐴 = 𝐵
3eqtr2i.2	⊢ 𝐶 = 𝐵
3eqtr2i.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtr2i	⊢ 𝐴 = 𝐷

Proof of Theorem 3eqtr2i

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr2i.2	. . 3 ⊢ 𝐶 = 𝐵
3	1, 2	eqtr4i 2755	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2752	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:  indif  4243  dfrab3  4282  iunidOLD  5025  cocnvcnv2  6231  fmptap  7144  cnvoprab  8039  fpar  8095  fodomr  9092  fodomfir  9279  jech9.3  9767  dju1dif  10126  alephadd  10530  distrnq  10914  ltanq  10924  ltrnq  10932  1p2e3  12324  halfpm6th  12404  numma  12693  numaddc  12697  6p5lem  12719  8p2e10  12729  binom2i  14177  faclbnd4lem1  14258  cats2cat  14828  0.999...  15847  flodddiv4  16385  6gcd4e2  16508  dfphi2  16744  mod2xnegi  17042  karatsuba  17054  1259lem1  17101  setc2obas  18056  oppgtopn  19285  symgplusg  19313  cmnbascntr  19735  mgptopn  20057  ply1plusg  22108  ply1vsca  22109  ply1mulr  22110  restcld  23059  cmpsublem  23286  kgentopon  23425  dfii5  24778  itg1climres  25615  pigt3  26427  ang180lem1  26719  1cubrlem  26751  quart1lem  26765  efiatan  26822  log2cnv  26854  log2ublem3  26858  1sgm2ppw  27111  ppiub  27115  bposlem8  27202  bposlem9  27203  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  bday1s  27743  addsasslem2  27911  seqsval  28182  ax5seglem7  28862  wlknwwlksnbij  29818  2pthd  29870  3pthd  30103  ipidsq  30639  ipdirilem  30758  norm3difi  31076  polid2i  31086  pjclem3  32126  cvmdi  32253  indifundif  32453  dpmul  32833  tocyccntz  33101  ccfldextdgrr  33667  cos9thpiminplylem5  33776  eulerpartlemt  34362  eulerpart  34373  ballotlem1  34478  ballotlemfval0  34487  ballotth  34529  hgt750lem  34642  hgt750lem2  34643  subfaclim  35175  kur14lem6  35198  quad3  35657  iexpire  35722  volsupnfl  37659  dfxrn2  38358  dmxrn  38360  xrninxp  38378  1p3e4  42247  ipiiie0  42426  sn-0tie0  42439  areaquad  43205  wallispilem4  46066  dirkertrigeqlem3  46098  dirkercncflem1  46101  fourierswlem  46228  fouriersw  46229  smflimsuplem8  46825  ceil5half3  47338  3exp4mod41  47614  41prothprm  47617  tgoldbachlt  47814  zlmodzxz0  48341  linevalexample  48381  mndtcco  49571