Theorem 3eqtr2 1501

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
3eqtr2	|- A = D

Proof of Theorem 3eqtr2

Step	Hyp	Ref	Expression
1		3eqtr2.1	. . 3 |- A = B
2		3eqtr2.2	. . 3 |- C = B
3	1, 2	eqtr4 1498	. 2 |- A = C
4		3eqtr2.3	. 2 |- C = D
5	3, 4	eqtr 1495	1 |- A = D

Syntax hints:   = wceq 956

This theorem is referenced by:  indif 2250  cocnvcnv2 3506  fodomr 4483  unir1 4667  halfpm6th 6032  crrecz 6741  ipcn 6790  faclbnd4lem1 6948  bcpasc2 6967  geolim1i 7238  reefcl 7317  efaddlem5 7342  ef4p 7399  efcnlem2 7420  cos2tOLD 7464  sin01bndlem1 7467  alephadd 7582  subtop 7646  ipid 8363  ip2i 8487  ipdirilem 8488  ipasslem10 8499  eulerid 8683  sincos6thpi 8711  norm3dif 9014  normpar2 9023  polid2 9024  projlem3 9188  hosd1 9748  lnophmlem2 9942  pjclem3 10125  fiv 10482  fivOLD 10483

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