Theorem 3eqtr3 1124

Description: An inference from three chained equalities.

Hypotheses

Ref	Expression
3eqtr3.1	⊢ A = B
3eqtr3.2	⊢ A = C
3eqtr3.3	⊢ B = D

Assertion

Ref	Expression
3eqtr3	⊢ C = D

Proof of Theorem 3eqtr3

Step	Hyp	Ref	Expression
1		3eqtr3.2	. 2 ⊢ A = C
2		3eqtr3.1	. . 3 ⊢ A = B
3		3eqtr3.3	. . 3 ⊢ B = D
4	2, 3	eqtr 1119	. 2 ⊢ A = D
5	1, 4	eqtr3 1121	1 ⊢ C = D

Syntax hints:   = wceq 1091

This theorem is referenced by:  un12 1616  in12 1651  difundi 1681  difundir 1682  difindi 1683  difindir 1684  difun1 1687  dif23 1688  difab 1693  iunab 2023  xp0 2652  caopr12 3075  caopr13 3077  caopr411 3079  caoprdistrr 3081  kmlem3 3582  cdaassen 3725  xpcdaen 3726  distrpq 3861  1pr 3911  reclem3pr 3952  pn0sr 4004  negneg 4154  mul12 4178  mulzer1 4185  negdi 4193  recrec 4253  ltadd2 4312  ltneg 4330  isqm1 4525  discrlem1 4713  nnesq 4720  nn0opthlem1 4722  sqr2irrlem1 4777  abslem2i 4866  fac0 4871  ruclem16 4900  ruclem25 4909  hvmulcom 5021  hvmul2neg 5022  hvadd12 5029  hvnegdi 5034  normlem1 5063  normlem8 5071  normpar2 5100  projlem3 5195  projlem18 5210  chjass 5407  chjo 5409  qlaxr3 5529  hos12 5608

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org