Theorem 3eqtri 2377

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

Syntax hints:   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  csbid  3143  un23  3422  in32  3467  dfrab2  3530  undifv  3624  undif2  3626  undifabs  3627  difun2  3629  difdifdir  3637  dfif4  3673  tpidm23  3823  unisn  3907  incompl  4073  pw10  4161  xpun  4834  dfdmf  4905  dfrnf  4962  res0  4977  resres  4980  resopab  4999  imai  5010  ima0  5013  epini  5021  imaundir  5040  dmtpop  5071  resdmres  5078  dmco  5089  coi2  5095  fvsnun1  5447  fvsnun2  5448  dmoprab  5574  rnoprab  5576  ov6g  5600  dmmpt  5683  rnmpt2  5717  cnvpprod  5841  mucid1  6143  sbthlem1  6203  scancan  6331