Theorem 3eqtr3ri 2235

Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr3ri	|- D = C

Proof of Theorem 3eqtr3ri

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

Syntax hints:   = wceq 1373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198

This theorem is referenced by:  indif2  3417  resdm2  5174  co01  5198  cocnvres  5208  undifdc  7023  1mhlfehlf  9257  rei  11243  resqrexlemover  11354  cos1bnd  12103  m1bits  12304  6gcd4e2  12349  3lcm2e6  12515  karatsuba  12786  cosq23lt0  15338  sincos4thpi  15345  sincos6thpi  15347  cosq34lt1  15355