Theorem 3eqtr2r 1494

Description: An inference from three chained equalities.

Hypotheses

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

Assertion

Ref	Expression
3eqtr2r	|- D = A

Proof of Theorem 3eqtr2r

Step	Hyp	Ref	Expression
1		3eqtr2.1	. 2 |- A = B
2		3eqtr2.2	. . 3 |- C = B
3	2	eqcomi 1471	. 2 |- B = C
4		3eqtr2.3	. 2 |- C = D
5	1, 3, 4	3eqtrr 1492	1 |- D = A

Syntax hints:   = wceq 953

This theorem is referenced by:  funimacnv 3557  1st2val 4079  2nd2val 4080  cardval2 4827  cjmulval 6727  sin01bndlem1 7409  cos2bnd 7417  ip0i 8415  polid2 8945  hh0v 8956  projlem3 9104  projlem4 9105  pjinorm 9538

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462

Copyright terms: Public domain