Theorem syl6req 1141

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

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

Proof of Theorem syl6req

Step	Hyp	Ref	Expression
1		syl6req.1	. . 3 |- (ph -> A = B)
2		syl6req.2	. . 3 |- B = C
3	1, 2	syl6eq 1140	. 2 |- (ph -> A = C)
4	3	cleqcomd 1106	1 |- (ph -> C = A)

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  syl6reqr 1143  reucl 1957  elxp4 2640  elxp5 2641  fvex 2838  fundmen 3333  xpsnen 3339  xpcomen 3343  xpassen 3344  inf5 3472  sqge0 4344  ine0 4524  alephsuc3 4955  hvmul0t 5004  dfchj3 5326  cmcmlem 5500  cmbr3 5509  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