Theorem syl6req 1521

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 1520	. 2 |- (ph -> A = C)
4	3	eqcomd 1477	1 |- (ph -> C = A)

Syntax hints:   -> wi 3   = wceq 954

This theorem is referenced by:  syl6reqr 1523  reucl 2880  elxp4 3445  elxp5 3446  fvex 3723  dfopab2 4103  dfoprab3 4104  oev2 4152  odi 4200  nneob 4245  fundmen 4415  xpsnen 4421  xpcomen 4425  xpassen 4427  infeq5 4601  ine0 5414  msqge0 5596  recexpt 6534  bcpasc 6915  ser1const 7115  efcvgfsum 7265  alephsuc3 7535  ismet 7748  metssba 7759  bcthlem10 7958  grprndm 8004  vafval 8174  smfval 8176  0vfval 8177  imsba 8272  minveclem38 8526  efif1lem5 8668  hvmul0t 8832  dfchj3 9263  cmcmlem 9474  cmbr3 9483  nmcoplb 9896  nmbdfnlb 9916  nmcfnlb 9925  cnlnadjlem5 9942  nmopcoadj 9972  pjin2 10059  hst1ht 10092  ghomfo 10325  domval 10535  codval 10536  idval 10537  cmpval 10538

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain