Theorem 3eqtri 2064

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 2060	. 2 |- B = D
5	1, 4	eqtri 2060	1 |- A = D

Syntax hints:   = wceq 1243

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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

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

This theorem is referenced by:  csbid  2859  un23  3102  in32  3149  dfrab2  3212  difun2  3302  tpidm23  3471  unisn  3596  dfiunv2  3693  uniop  3992  suc0  4148  unisuc  4150  iunsuc  4157  xpun  4401  dfrn2  4523  dfdmf  4528  dfrnf  4575  res0  4616  resres  4624  xpssres  4645  dfima2  4670  imai  4681  ima0  4684  imaundir  4737  xpima1  4767  xpima2m  4768  dmresv  4779  rescnvcnv  4783  dmtpop  4796  rnsnopg  4799  resdmres  4812  dmmpt  4816  dmco  4829  co01  4835  fpr  5345  fmptpr  5355  fvsnun2  5361  mpt20  5574  dmoprab  5585  rnoprab  5587  ov6g  5638  1st0  5771  2nd0  5772  dfmpt2  5844  algrflem  5850  dftpos2  5876  tposoprab  5895  tposmpt2  5896  tfrlem8  5934  df2o3  6014  axi2m1  6949  2p2e4  8037  numsuc  8379  numsucc  8393  xnegmnf  8742  fz0tp  8981  fzo0to2pr  9074  fzo0to3tp  9075  fzo0to42pr  9076  i4  9355  abs0  9656  absi  9657