Theorem 3eqtr2i 2760

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  indif  4227  dfrab3  4266  cocnvcnv2  6206  fmptap  7104  cnvoprab  7992  fpar  8046  fodomr  9041  fodomfir  9212  jech9.3  9707  dju1dif  10064  alephadd  10468  distrnq  10852  ltanq  10862  ltrnq  10870  1p2e3  12263  halfpm6th  12343  numma  12632  numaddc  12636  6p5lem  12658  8p2e10  12668  binom2i  14119  faclbnd4lem1  14200  cats2cat  14769  0.999...  15788  flodddiv4  16326  6gcd4e2  16449  dfphi2  16685  mod2xnegi  16983  karatsuba  16995  1259lem1  17042  setc2obas  18001  oppgtopn  19265  symgplusg  19295  cmnbascntr  19717  mgptopn  20066  ply1plusg  22136  ply1vsca  22137  ply1mulr  22138  restcld  23087  cmpsublem  23314  kgentopon  23453  dfii5  24805  itg1climres  25642  pigt3  26454  ang180lem1  26746  1cubrlem  26778  quart1lem  26792  efiatan  26849  log2cnv  26881  log2ublem3  26885  1sgm2ppw  27138  ppiub  27142  bposlem8  27229  bposlem9  27230  2lgsoddprmlem3c  27350  2lgsoddprmlem3d  27351  bday1s  27775  addsasslem2  27947  seqsval  28218  ax5seglem7  28913  wlknwwlksnbij  29866  2pthd  29918  3pthd  30154  ipidsq  30690  ipdirilem  30809  norm3difi  31127  polid2i  31137  pjclem3  32177  cvmdi  32304  indifundif  32504  dpmul  32893  tocyccntz  33113  ccfldextdgrr  33685  cos9thpiminplylem5  33799  eulerpartlemt  34384  eulerpart  34395  ballotlem1  34500  ballotlemfval0  34509  ballotth  34551  hgt750lem  34664  hgt750lem2  34665  subfaclim  35232  kur14lem6  35255  quad3  35714  iexpire  35779  volsupnfl  37713  dfxrn2  38412  dmxrn  38414  xrninxp  38432  1p3e4  42300  ipiiie0  42479  sn-0tie0  42492  areaquad  43257  wallispilem4  46114  dirkertrigeqlem3  46146  dirkercncflem1  46149  fourierswlem  46276  fouriersw  46277  smflimsuplem8  46873  ceil5half3  47379  3exp4mod41  47655  41prothprm  47658  tgoldbachlt  47855  zlmodzxz0  48395  linevalexample  48435  mndtcco  49625