Theorem 3eqtrr 1500

Description: An inference from three chained equalities.

Hypotheses

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

Assertion

Ref	Expression
3eqtrr	|- D = A

Proof of Theorem 3eqtrr

Step	Hyp	Ref	Expression
1		3eqtr.3	. 2 |- C = D
2		3eqtr.1	. . 3 |- A = B
3		3eqtr.2	. . 3 |- B = C
4	2, 3	eqtr2 1496	. 2 |- C = A
5	1, 4	eqtr3 1497	1 |- D = A

Syntax hints:   = wceq 956

This theorem is referenced by:  3eqtr2r 1502  cofunex2g 3581  discrlem1 6656  sqrlem2 6674  fnsmnt 7226  0.999... 7246  ruclem1 7510  ruclem3 7512  cnnvg 8308  cnnvs 8311  cnnvnm 8312  ipdirilem 8488  minveclem27 8571  sincosq3sgn 8706  sincosq4sgn 8707  sincos4thpi 8710  h2hva 8843  h2hsm 8844  h2hnm 8845  hhssva 9129  hhsssm 9130  hhssnm 9131  spansnj 9591  lnopunilem1 9935  lnophmlem2 9942  stadd3 10175  mapudiscn 10512  eqindhome 10541

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