Theorem eqtr2 1120

Description: An equality transitivity inference.

Hypotheses

Ref	Expression
eqtr2.1	|- A = B
eqtr2.2	|- B = C

Assertion

Ref	Expression
eqtr2	|- C = A

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqtr2.1	. . 3 |- A = B
2		eqtr2.2	. . 3 |- B = C
3	1, 2	eqtr 1119	. 2 |- A = C
4	3	cleqcomi 1105	1 |- C = A

Syntax hints:   = wceq 1091

This theorem is referenced by:  3eqtr4r 1127  dfun3 1671  symdif1 1689  dfsn2 1819  prprc 1839  unidif0 1944  epfrc 2185  xpindi 2497  xpindir 2498  resabs1 2592  co01 2664  f1cnv 2782  tz7.44-2 2967  sbthlem8 3356  mapenlem2 3385  fiint 3445  trcl 3489  neg11 4164  eqneg 4378  discrlem1 4713  sqrlem2 4732  sqrlem11 4741  ipcn 4820  abslem2i 4866  ruclem1 4885  ruclem3 4887  ruclem10 4894  ruclem11 4895  normlem6 5068  norm3dif 5094  occllem1 5180  projlem4 5196  projlem18 5210  pjthlem1 5225  pjthlem5 5229  pjthlem14 5238  h1de2 5458  spansnj 5539  pjclem1 5649  pjnel 5665  stadd3 5689

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