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  3144  un23  3423  in32  3468  dfrab2  3531  undifv  3625  undif2  3627  undifabs  3628  difun2  3630  difdifdir  3638  dfif4  3674  tpidm23  3824  unisn  3908  incompl  4074  pw10  4162  xpun  4835  dfdmf  4906  dfrnf  4963  res0  4978  resres  4981  resopab  5000  imai  5011  ima0  5014  epini  5022  imaundir  5041  dmtpop  5072  resdmres  5079  dmco  5090  coi2  5096  fvsnun1  5448  fvsnun2  5449  dmoprab  5575  rnoprab  5577  ov6g  5601  dmmpt  5684  rnmpt2  5718  cnvpprod  5842  mucid1  6144  sbthlem1  6204  scancan  6332