Theorem 3eqtr2i 2810

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

Syntax hints:   = wceq 1508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-9 2060  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-cleq 2773

This theorem is referenced by:  indif  4136  dfrab3  4168  iunid  4855  cocnvcnv2  5955  fmptap  6761  cnvoprab  7572  fpar  7625  fodomr  8470  jech9.3  9043  dju1dif  9402  alephadd  9803  distrnq  10187  ltanq  10197  ltrnq  10205  1p2e3  11596  halfpm6th  11674  numma  11962  numaddc  11966  6p5lem  11989  8p2e10  11999  binom2i  13395  faclbnd4lem1  13474  cats2cat  14092  0.999...  15103  flodddiv4  15630  6gcd4e2  15748  dfphi2  15973  mod2xnegi  16269  karatsuba  16282  1259lem1  16326  oppgtopn  18264  mgptopn  18983  ply1plusg  20111  ply1vsca  20112  ply1mulr  20113  restcld  21499  cmpsublem  21726  kgentopon  21865  txswaphmeolem  22131  dfii5  23211  itg1climres  24033  pigt3  24821  ang180lem1  25103  1cubrlem  25135  quart1lem  25149  efiatan  25206  log2cnv  25239  log2ublem3  25243  1sgm2ppw  25493  ppiub  25497  bposlem8  25584  bposlem9  25585  2lgsoddprmlem3c  25705  2lgsoddprmlem3d  25706  ax5seglem7  26439  wlknwwlksnbij  27390  2pthd  27461  3pthd  27718  ipidsq  28279  ipdirilem  28398  norm3difi  28718  polid2i  28728  pjclem3  29770  cvmdi  29897  indifundif  30074  dpmul  30359  ccfldextdgrr  30718  eulerpartlemt  31306  eulerpart  31317  ballotlem1  31422  ballotlemfval0  31431  ballotth  31473  hgt750lem  31602  hgt750lem2  31603  subfaclim  32060  kur14lem6  32083  quad3  32473  iexpire  32527  volsupnfl  34418  dfxrn2  35113  xrninxp  35125  areaquad  39260  wallispilem4  41819  dirkertrigeqlem3  41851  dirkercncflem1  41854  fourierswlem  41981  fouriersw  41982  smflimsuplem8  42567  3exp4mod41  43184  41prothprm  43187  tgoldbachlt  43384  zlmodzxz0  43803  linevalexample  43852