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-1 5  ax-2 6  ax-3 7  ax-mp 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  3200  dfin3  3494  dfin5  3545  dfif6  3665  qdass  3819  tpidm12  3821  ssfin  4470  nnadjoin  4520  nulnnn  4556  df1st2  4738  dfsset2  4743  dfco1  4748  dfsi2  4751  resres  4980  inres  4985  cnvun  5033  coundi  5082  coundir  5083  snec  5987  df0c2  6137  1cnc  6139  1p1e2c  6155  2p1e3c  6156