Theorem 3eqtrr 1503

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 1499	. 2 ⊢ C = A
5	1, 4	eqtr3 1500	1 ⊢ D = A

Syntax hints:   = wceq 958

This theorem is referenced by:  3eqtr2r 1505  cofunex2g 3587  discrlem1 6657  sqrlem2 6675  fnsmnt 7226  0.999... 7246  ruclem1 7511  ruclem3 7513  cnnvg 8304  cnnvs 8307  cnnvnm 8308  ipdirilem 8484  minveclem27 8567  sincosq3sgn 8701  sincosq4sgn 8702  sincos4thpi 8705  h2hva 8838  h2hsm 8839  h2hnm 8840  hhssva 9124  hhsssm 9125  hhssnm 9126  spansnj 9586  lnopunilem1 9930  lnophmlem2 9937  stadd3 10170  mapudiscn 10498  eqindhome 10527

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain