Theorem 3eqtr2i 2792

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 2789	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2786	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  indif  4233  dfrab3  4272  cocnvcnv2  6260  fmptap  7168  cnvoprab  8053  fpar  8107  fodomr  9112  fodomfir  9283  jech9.3  9782  dju1dif  10152  alephadd  10557  distrnq  10941  ltanq  10951  ltrnq  10959  1p2e3  12378  halfpm6th  12461  numma  12755  numaddc  12759  6p5lem  12781  8p2e10  12791  binom2i  14244  faclbnd4lem1  14325  cats2cat  14895  0.999...  15931  flodddiv4  16468  6gcd4e2  16591  dfphi2  16828  mod2xnegi  17126  karatsuba  17138  1259lem1  17186  setc2obas  18146  oppgtopn  19418  symgplusg  19448  cmnbascntr  19870  mgptopn  20219  ply1plusg  22383  ply1vsca  22384  ply1mulr  22385  restcld  23329  cmpsublem  23556  kgentopon  23695  dfii5  25044  itg1climres  25873  pigt3  26683  ang180lem1  26974  1cubrlem  27006  quart1lem  27020  efiatan  27077  log2cnv  27109  log2ublem3  27113  1sgm2ppw  27364  ppiub  27368  bposlem8  27455  bposlem9  27456  2lgsoddprmlem3c  27576  2lgsoddprmlem3d  27577  bday1  28007  addsasslem2  28197  seqsval  28481  ax5seglem7  29285  wlknwwlksnbij  30237  2pthd  30289  3pthd  30525  ipidsq  31062  ipdirilem  31181  norm3difi  31499  polid2i  31509  pjclem3  32549  cvmdi  32676  indifundif  32870  dpmul  33232  tocyccntz  33464  ccfldextdgrr  34062  cos9thpiminplylem5  34176  eulerpartlemt  34761  eulerpart  34772  ballotlem1  34877  ballotlemfval0  34886  ballotth  34928  hgt750lem  35038  hgt750lem2  35039  subfaclim  35680  kur14lem6  35703  quad3  36162  iexpire  36227  volsupnfl  38316  dfxrn2  39034  dmxrn  39036  dmxrnuncnvepres  39041  xrninxp  39064  1p3e4  43026  ipiiie0  43199  sn-0tie0  43225  areaquad  43943  wallispilem4  46782  dirkertrigeqlem3  46814  dirkercncflem1  46817  fourierswlem  46944  fouriersw  46945  smflimsuplem8  47541  ceil5half3  48083  3exp4mod41  48368  41prothprm  48371  tgoldbachlt  48581  zlmodzxz0  49136  linevalexample  49175  mndtcco  50363