Theorem syl5reqr 1139

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

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

Proof of Theorem syl5reqr

Step	Hyp	Ref	Expression
1		syl5reqr.1	. 2 |- (ph -> A = B)
2		syl5reqr.2	. . 3 |- A = C
3	2	cleqcomi 1105	. 2 |- C = A
4	1, 3	syl5req 1137	1 |- (ph -> B = C)

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  limsuclem 2360  resabs1 2592  coi2 2666  fnima 2738  foima 2790  f1imacnv 2814  f1o00 2823  mapsn 3269  sbthlem4 3352  sbthlem6 3354  pssnn 3428  prlem934a 3931  discrlem3 4715  pjssm 5572  cvexchlem 5759

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