Theorem 3eqtr2i 2759

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

Syntax hints:   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  indif  4268  dfrab3  4308  iunidOLD  5065  cocnvcnv2  6264  fmptap  7179  cnvoprab  8065  fpar  8121  fodomr  9153  jech9.3  9839  dju1dif  10197  alephadd  10602  distrnq  10986  ltanq  10996  ltrnq  11004  1p2e3  12388  halfpm6th  12466  numma  12754  numaddc  12758  6p5lem  12780  8p2e10  12790  binom2i  14211  faclbnd4lem1  14288  cats2cat  14849  0.999...  15863  flodddiv4  16393  6gcd4e2  16517  dfphi2  16746  mod2xnegi  17043  karatsuba  17056  1259lem1  17103  setc2obas  18086  oppgtopn  19319  symgplusg  19349  cmnbascntr  19772  mgptopn  20098  ply1plusg  22166  ply1vsca  22167  ply1mulr  22168  restcld  23120  cmpsublem  23347  kgentopon  23486  dfii5  24849  itg1climres  25688  pigt3  26497  ang180lem1  26786  1cubrlem  26818  quart1lem  26832  efiatan  26889  log2cnv  26921  log2ublem3  26925  1sgm2ppw  27178  ppiub  27182  bposlem8  27269  bposlem9  27270  2lgsoddprmlem3c  27390  2lgsoddprmlem3d  27391  bday1s  27810  addsasslem2  27967  seqsval  28211  ax5seglem7  28818  wlknwwlksnbij  29771  2pthd  29823  3pthd  30056  ipidsq  30592  ipdirilem  30711  norm3difi  31029  polid2i  31039  pjclem3  32079  cvmdi  32206  indifundif  32400  dpmul  32721  tocyccntz  32957  ccfldextdgrr  33491  eulerpartlemt  34122  eulerpart  34133  ballotlem1  34237  ballotlemfval0  34246  ballotth  34288  hgt750lem  34414  hgt750lem2  34415  subfaclim  34929  kur14lem6  34952  quad3  35405  iexpire  35460  volsupnfl  37269  dfxrn2  37978  xrninxp  37994  ipiiie0  42127  sn-0tie0  42129  areaquad  42786  wallispilem4  45594  dirkertrigeqlem3  45626  dirkercncflem1  45629  fourierswlem  45756  fouriersw  45757  smflimsuplem8  46353  3exp4mod41  47093  41prothprm  47096  tgoldbachlt  47293  zlmodzxz0  47606  linevalexample  47649  mndtcco  48283