Theorem 3eqtr4ri 2384

Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr4ri	|- D = C

Proof of Theorem 3eqtr4ri

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

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:  cbvreucsf  3201  dfin3  3495  dfin5  3546  dfif6  3666  qdass  3820  tpidm12  3822  ssfin  4471  nnadjoin  4521  nulnnn  4557  df1st2  4739  dfsset2  4744  dfco1  4749  dfsi2  4752  resres  4981  inres  4986  cnvun  5034  coundi  5083  coundir  5084  snec  5988  df0c2  6138  1cnc  6140  1p1e2c  6156  2p1e3c  6157