Theorem syl6reqr 2189

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 2141	. 2 |- B = C
4	1, 3	syl6req 2187	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 2119

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

This theorem is referenced by:  iftrue  3474  iffalse  3477  difprsn1  3654  dmmptg  5031  relcoi1  5065  funimacnv  5194  dmmptd  5248  dffv3g  5410  dfimafn  5463  fvco2  5483  isoini  5712  oprabco  6107  ixpconstg  6594  unfiexmid  6799  undifdc  6805  sbthlemi4  6841  sbthlemi5  6842  sbthlemi6  6843  supval2ti  6875  exmidfodomrlemim  7050  suplocexprlemex  7523  eqneg  8485  zeo  9149  fseq1p1m1  9867  seq3val  10224  seqvalcd  10225  hashfzo  10561  hashxp  10565  fsumconst  11216  modfsummod  11220  telfsumo  11228  mulgcd  11693  algcvg  11718  phiprmpw  11887  strslfv3  11993  uptx  12432  resubmet  12706