Theorem 3eqtr2i 2770

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728

This theorem is referenced by:  indif  4279  dfrab3  4318  iunidOLD  5060  cocnvcnv2  6277  fmptap  7191  cnvoprab  8086  fpar  8142  fodomr  9169  fodomfir  9369  jech9.3  9855  dju1dif  10214  alephadd  10618  distrnq  11002  ltanq  11012  ltrnq  11020  1p2e3  12410  halfpm6th  12490  numma  12779  numaddc  12783  6p5lem  12805  8p2e10  12815  binom2i  14252  faclbnd4lem1  14333  cats2cat  14902  0.999...  15918  flodddiv4  16453  6gcd4e2  16576  dfphi2  16812  mod2xnegi  17110  karatsuba  17122  1259lem1  17169  setc2obas  18140  oppgtopn  19373  symgplusg  19401  cmnbascntr  19824  mgptopn  20146  ply1plusg  22226  ply1vsca  22227  ply1mulr  22228  restcld  23181  cmpsublem  23408  kgentopon  23547  dfii5  24912  itg1climres  25750  pigt3  26561  ang180lem1  26853  1cubrlem  26885  quart1lem  26899  efiatan  26956  log2cnv  26988  log2ublem3  26992  1sgm2ppw  27245  ppiub  27249  bposlem8  27336  bposlem9  27337  2lgsoddprmlem3c  27457  2lgsoddprmlem3d  27458  bday1s  27877  addsasslem2  28038  seqsval  28295  pw2bday  28419  ax5seglem7  28951  wlknwwlksnbij  29909  2pthd  29961  3pthd  30194  ipidsq  30730  ipdirilem  30849  norm3difi  31167  polid2i  31177  pjclem3  32217  cvmdi  32344  indifundif  32544  dpmul  32896  tocyccntz  33165  ccfldextdgrr  33723  eulerpartlemt  34374  eulerpart  34385  ballotlem1  34490  ballotlemfval0  34499  ballotth  34541  hgt750lem  34667  hgt750lem2  34668  subfaclim  35194  kur14lem6  35217  quad3  35676  iexpire  35736  volsupnfl  37673  dfxrn2  38378  xrninxp  38394  ipiiie0  42472  sn-0tie0  42474  areaquad  43233  wallispilem4  46088  dirkertrigeqlem3  46120  dirkercncflem1  46123  fourierswlem  46250  fouriersw  46251  smflimsuplem8  46847  ceil5half3  47347  3exp4mod41  47608  41prothprm  47611  tgoldbachlt  47808  zlmodzxz0  48277  linevalexample  48317  mndtcco  49237