Theorem 3eqtr2i 2765

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 2762	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2759	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 2708

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

This theorem is referenced by:  indif  4260  dfrab3  4299  iunidOLD  5042  cocnvcnv2  6252  fmptap  7167  cnvoprab  8064  fpar  8120  fodomr  9147  fodomfir  9345  jech9.3  9833  dju1dif  10192  alephadd  10596  distrnq  10980  ltanq  10990  ltrnq  10998  1p2e3  12388  halfpm6th  12468  numma  12757  numaddc  12761  6p5lem  12783  8p2e10  12793  binom2i  14235  faclbnd4lem1  14316  cats2cat  14886  0.999...  15902  flodddiv4  16439  6gcd4e2  16562  dfphi2  16798  mod2xnegi  17096  karatsuba  17108  1259lem1  17155  setc2obas  18112  oppgtopn  19341  symgplusg  19369  cmnbascntr  19791  mgptopn  20113  ply1plusg  22164  ply1vsca  22165  ply1mulr  22166  restcld  23115  cmpsublem  23342  kgentopon  23481  dfii5  24834  itg1climres  25672  pigt3  26484  ang180lem1  26776  1cubrlem  26808  quart1lem  26822  efiatan  26879  log2cnv  26911  log2ublem3  26915  1sgm2ppw  27168  ppiub  27172  bposlem8  27259  bposlem9  27260  2lgsoddprmlem3c  27380  2lgsoddprmlem3d  27381  bday1s  27800  addsasslem2  27968  seqsval  28239  ax5seglem7  28919  wlknwwlksnbij  29875  2pthd  29927  3pthd  30160  ipidsq  30696  ipdirilem  30815  norm3difi  31133  polid2i  31143  pjclem3  32183  cvmdi  32310  indifundif  32510  dpmul  32892  tocyccntz  33160  ccfldextdgrr  33718  cos9thpiminplylem5  33825  eulerpartlemt  34408  eulerpart  34419  ballotlem1  34524  ballotlemfval0  34533  ballotth  34575  hgt750lem  34688  hgt750lem2  34689  subfaclim  35215  kur14lem6  35238  quad3  35697  iexpire  35757  volsupnfl  37694  dfxrn2  38399  xrninxp  38415  ipiiie0  42447  sn-0tie0  42449  areaquad  43207  wallispilem4  46064  dirkertrigeqlem3  46096  dirkercncflem1  46099  fourierswlem  46226  fouriersw  46227  smflimsuplem8  46823  ceil5half3  47336  3exp4mod41  47597  41prothprm  47600  tgoldbachlt  47797  zlmodzxz0  48298  linevalexample  48338  mndtcco  49429