Theorem 3eqtr2 1504

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 1501	. 2 ⊢ A = C
4		3eqtr2.3	. 2 ⊢ C = D
5	3, 4	eqtr 1498	1 ⊢ A = D

Syntax hints:   = wceq 958

This theorem is referenced by:  indif 2253  cocnvcnv2 3512  fodomr 4489  unir1 4677  halfpm6th 6034  crrecz 6742  ipcn 6790  faclbnd4lem1 6948  bcpasc2 6967  geolim1i 7238  reefcl 7317  efaddlem5 7342  ef4p 7399  efcnlem2 7420  cos2tOLD 7465  sin01bndlem1 7468  alephadd 7584  subtop 7643  ipid 8359  ip2i 8483  ipdirilem 8484  ipasslem10 8495  eulerid 8678  sincos6thpi 8706  norm3dif 9009  normpar2 9018  polid2 9019  projlem3 9183  hosd1 9743  lnophmlem2 9937  pjclem3 10120  fiv 10470

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