Theorem 3eqtr2i 2650

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2i.1	|- A = B
3eqtr2i.2	|- C = B
3eqtr2i.3	|- C = D

Assertion

Ref	Expression
3eqtr2i	|- A = D

Proof of Theorem 3eqtr2i

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 |- A = B
2		3eqtr2i.2	. . 3 |- C = B
3	1, 2	eqtr4i 2647	. 2 |- A = C
4		3eqtr2i.3	. 2 |- C = D
5	3, 4	eqtri 2644	1 |- A = D

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  indif  3869  dfrab3  3902  iunid  4575  cnvcnvOLD  5587  cocnvcnv2  5647  fmptap  6436  fpar  7281  fodomr  8111  jech9.3  8677  cda1dif  8998  alephadd  9399  distrnq  9783  ltanq  9793  ltrnq  9801  halfpm6th  11253  numma  11557  numaddc  11561  6p5lem  11595  8p2e10  11610  binom2i  12974  faclbnd4lem1  13080  cats2cat  13607  0.999...  14612  0.999...OLD  14613  flodddiv4  15137  6gcd4e2  15255  dfphi2  15479  mod2xnegi  15775  karatsuba  15792  karatsubaOLD  15793  1259lem1  15838  oppgtopn  17783  mgptopn  18498  ply1plusg  19595  ply1vsca  19596  ply1mulr  19597  restcld  20976  cmpsublem  21202  kgentopon  21341  txswaphmeolem  21607  dfii5  22688  itg1climres  23481  ang180lem1  24539  1cubrlem  24568  quart1lem  24582  efiatan  24639  log2cnv  24671  log2ublem3  24675  1sgm2ppw  24925  ppiub  24929  bposlem8  25016  bposlem9  25017  2lgsoddprmlem3c  25137  2lgsoddprmlem3d  25138  ax5seglem7  25815  2pthd  26836  3pthd  27034  ipidsq  27565  ipdirilem  27684  norm3difi  28004  polid2i  28014  pjclem3  29056  cvmdi  29183  indifundif  29356  dpmul  29621  eulerpartlemt  30433  eulerpart  30444  ballotlem1  30548  ballotlemfval0  30557  ballotth  30599  hgt750lem  30729  hgt750lem2  30730  subfaclim  31170  kur14lem6  31193  quad3  31564  iexpire  31621  pigt3  33402  volsupnfl  33454  areaquad  37802  wallispilem4  40285  dirkertrigeqlem3  40317  dirkercncflem1  40320  fourierswlem  40447  fouriersw  40448  smflimsuplem8  41033  3exp4mod41  41533  41prothprm  41536  tgoldbachlt  41704  tgoldbachltOLD  41710  zlmodzxz0  42134  linevalexample  42184