Theorem 3eqtr2r 1502

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 1479	. 2 |- B = C
4		3eqtr2.3	. 2 |- C = D
5	1, 3, 4	3eqtrr 1500	1 |- D = A

Syntax hints:   = wceq 956

This theorem is referenced by:  funimacnv 3571  1st2val 4095  2nd2val 4096  cardval2 4855  cjmulval 6792  sin01bndlem1 7467  cos2bnd 7475  ip0i 8484  polid2 9024  hh0v 9035  projlem3 9188  projlem4 9189  pjinorm 9621

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain