Theorem 3eqtri 2061

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

Hypotheses

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

Assertion

Ref	Expression
3eqtri	|- A = D

Proof of Theorem 3eqtri

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 |- A = B
2		3eqtri.2	. . 3 |- B = C
3		3eqtri.3	. . 3 |- C = D
4	2, 3	eqtri 2057	. 2 |- B = D
5	1, 4	eqtri 2057	1 |- A = D

Syntax hints:   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  csbid  2853  un23  3096  in32  3143  dfrab2  3206  difun2  3296  tpidm23  3462  unisn  3587  dfiunv2  3684  uniop  3983  suc0  4114  unisuc  4116  iunsuc  4123  xpun  4344  dfrn2  4466  dfdmf  4471  dfrnf  4518  res0  4559  resres  4567  xpssres  4588  dfima2  4613  imai  4624  ima0  4627  imaundir  4680  xpima1  4710  xpima2m  4711  dmresv  4722  rescnvcnv  4726  dmtpop  4739  rnsnopg  4742  resdmres  4755  dmmpt  4759  dmco  4772  co01  4778  fpr  5288  fmptpr  5298  fvsnun2  5304  mpt20  5516  dmoprab  5527  rnoprab  5529  ov6g  5580  1st0  5713  2nd0  5714  dfmpt2  5786  algrflem  5792  dftpos2  5817  tposoprab  5836  tposmpt2  5837  tfrlem8  5875  df2o3  5953  axi2m1  6759  2p2e4  7815  numsuc  8155  numsucc  8169  xnegmnf  8512  fz0tp  8751  fzo0to2pr  8844  fzo0to3tp  8845  fzo0to42pr  8846  i4  9008  abs0  9222  absi  9223