Theorem 3eqtr2i 2769

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  indif  4286  dfrab3  4325  iunidOLD  5066  cocnvcnv2  6280  fmptap  7190  cnvoprab  8084  fpar  8140  fodomr  9167  fodomfir  9366  jech9.3  9852  dju1dif  10211  alephadd  10615  distrnq  10999  ltanq  11009  ltrnq  11017  1p2e3  12407  halfpm6th  12485  numma  12775  numaddc  12779  6p5lem  12801  8p2e10  12811  binom2i  14248  faclbnd4lem1  14329  cats2cat  14898  0.999...  15914  flodddiv4  16449  6gcd4e2  16572  dfphi2  16808  mod2xnegi  17105  karatsuba  17118  1259lem1  17165  setc2obas  18148  oppgtopn  19387  symgplusg  19415  cmnbascntr  19838  mgptopn  20164  ply1plusg  22241  ply1vsca  22242  ply1mulr  22243  restcld  23196  cmpsublem  23423  kgentopon  23562  dfii5  24925  itg1climres  25764  pigt3  26575  ang180lem1  26867  1cubrlem  26899  quart1lem  26913  efiatan  26970  log2cnv  27002  log2ublem3  27006  1sgm2ppw  27259  ppiub  27263  bposlem8  27350  bposlem9  27351  2lgsoddprmlem3c  27471  2lgsoddprmlem3d  27472  bday1s  27891  addsasslem2  28052  seqsval  28309  pw2bday  28433  ax5seglem7  28965  wlknwwlksnbij  29918  2pthd  29970  3pthd  30203  ipidsq  30739  ipdirilem  30858  norm3difi  31176  polid2i  31186  pjclem3  32226  cvmdi  32353  indifundif  32552  dpmul  32880  tocyccntz  33147  ccfldextdgrr  33697  eulerpartlemt  34353  eulerpart  34364  ballotlem1  34468  ballotlemfval0  34477  ballotth  34519  hgt750lem  34645  hgt750lem2  34646  subfaclim  35173  kur14lem6  35196  quad3  35655  iexpire  35715  volsupnfl  37652  dfxrn2  38358  xrninxp  38374  ipiiie0  42444  sn-0tie0  42446  areaquad  43205  wallispilem4  46024  dirkertrigeqlem3  46056  dirkercncflem1  46059  fourierswlem  46186  fouriersw  46187  smflimsuplem8  46783  ceil5half3  47280  3exp4mod41  47541  41prothprm  47544  tgoldbachlt  47741  zlmodzxz0  48201  linevalexample  48241  mndtcco  48894