Theorem syl6reqr 1143

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
syl6reqr	|- (ph -> C = A)

Proof of Theorem syl6reqr

Step	Hyp	Ref	Expression
1		syl6reqr.1	. 2 |- (ph -> A = B)
2		syl6reqr.2	. . 3 |- C = B
3	2	cleqcomi 1105	. 2 |- B = C
4	1, 3	syl6req 1141	1 |- (ph -> C = A)

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  iftrue 1780  iffalse 1781  resabs1 2592  resabs2 2593  funimacnv 2711  zfrep6 2744  isoini 2938  sbthlem4 3352  sbthlem5 3353  sbthlem6 3354  mapunen 3397  aceq3 3556  cardval 3633  alephsuc2 3686  pjclem2 5650

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