Theorem syl6reqr 2140

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

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	eqcomi 2093	. 2 |- B = C
4	1, 3	syl6req 2138	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-cleq 2082

This theorem is referenced by:  iftrue  3402  iffalse  3405  difprsn1  3582  dmmptg  4941  relcoi1  4975  funimacnv  5103  dffv3g  5314  dfimafn  5366  fvco2  5386  isoini  5611  oprabco  5996  ixpconstg  6478  unfiexmid  6682  undifdc  6688  sbthlemi4  6723  sbthlemi5  6724  sbthlemi6  6725  supval2ti  6744  exmidfodomrlemim  6881  eqneg  8253  zeo  8905  fseq1p1m1  9562  iseqval  9925  iseqvalt  9927  seq3val  9928  hashfzo  10284  hashxp  10288  fsumconst  10902  modfsummod  10906  telfsumo  10914  mulgcd  11337  algcvg  11362  phiprmpw  11530  strslfv3  11593