Theorem 3eqtr4r 1127

Description: An inference from three chained equalities.

Hypotheses

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

Assertion

Ref	Expression
3eqtr4r	|- D = C

Proof of Theorem 3eqtr4r

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

Syntax hints:   = wceq 1091

This theorem is referenced by:  dfin3 1672  difdifdir 1765  unpr 1930  unidif0 1944  iunrab 2022  dfdm4 2525  dmsnsnsn 2548  1st2val 3097  axmulass 4073  divmul13 4267  3p2e5 4492  4p2e6 4494  5p2e7 4497  6p2e8 4500  7p2e9 4502  nnesq 4720  sqrmuli 4762  abs3dif 4860  infmap2 4953  normlem2 5064  bcseq 5073  cmcmlem 5500  spansnj 5539  pjadj 5564

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