Theorem syl6reqr 2191

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  iftrue  3479  iffalse  3482  difprsn1  3659  dmmptg  5036  relcoi1  5070  funimacnv  5199  dmmptd  5253  dffv3g  5417  dfimafn  5470  fvco2  5490  isoini  5719  oprabco  6114  ixpconstg  6601  unfiexmid  6806  undifdc  6812  sbthlemi4  6848  sbthlemi5  6849  sbthlemi6  6850  supval2ti  6882  exmidfodomrlemim  7057  suplocexprlemex  7530  eqneg  8492  zeo  9156  fseq1p1m1  9874  seq3val  10231  seqvalcd  10232  hashfzo  10568  hashxp  10572  fsumconst  11223  modfsummod  11227  telfsumo  11235  mulgcd  11704  algcvg  11729  phiprmpw  11898  strslfv3  12004  uptx  12443  resubmet  12717