Theorem syl5eqr 1138

Description: An equality transitivity deduction.

Hypotheses

Ref	Expression
syl5eqr.1	|- (ph -> A = B)
syl5eqr.2	|- A = C

Assertion

Ref	Expression
syl5eqr	|- (ph -> C = B)

Proof of Theorem syl5eqr

Step	Hyp	Ref	Expression
1		syl5eqr.1	. 2 |- (ph -> A = B)
2		syl5eqr.2	. . 3 |- A = C
3	2	cleqcomi 1105	. 2 |- C = A
4	1, 3	syl5eq 1136	1 |- (ph -> C = B)

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  3eqtr3g 1146  fnex 2740  f1ocnv 2811  f1imacnv 2814  funfv 2862  fsn2 2896  oasuc 3131  omsuc 3133  oesuc 3134  pw2en 3348  sbthlem8 3356  sbthlem9 3357  fiint 3445  inf3lem7 3470  fodom 3613  fodomb 3615  prlem934a 3931  reclem3pr 3952  pn0sr 4004  mulgt0sr 4008  supsrlem2 4020  addge0 4324  addgegt0 4325  add20 4329  mulge0 4335  rimul 4534  sqrcl 4758  sqrge0 4760  rere 4810  absnid 4851  hizer1t 5054  pjch 5269  chjidmt 5436  pjch0t 5562  pjin2 5647

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