Theorem syl6reqr 2132

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

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  iftrue  3356  iffalse  3359  difprsn1  3525  dmmptg  4838  relcoi1  4869  funimacnv  4995  dffv3g  5194  dfimafn  5243  fvco2  5263  isoini  5477  oprabco  5858  supval2ti  6408  eqneg  7820  zeo  8452  fseq1p1m1  9111  iseqval  9440  mulgcd  10405  ialgrp1  10428  ialgcvg  10430