Theorem syl6eqr 2131

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl6eqr.1	|- ( ph -> A = B )
syl6eqr.2	|- C = B

Assertion

Ref	Expression
syl6eqr	|- ( ph -> A = C )

Proof of Theorem syl6eqr

Step	Hyp	Ref	Expression
1		syl6eqr.1	. 2 |- ( ph -> A = B )
2		syl6eqr.2	. . 3 |- C = B
3	2	eqcomi 2085	. 2 |- B = C
4	1, 3	syl6eq 2129	1 |- ( ph -> A = C )

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:  3eqtr4g  2138  rabxmdc  3276  relop  4504  csbcnvg  4537  dfiun3g  4607  dfiin3g  4608  resima2  4662  relcnvfld  4871  uniabio  4897  fntpg  4975  dffn5im  5240  dfimafn2  5244  fncnvima2  5309  fmptcof  5352  fcoconst  5355  fnasrng  5364  ffnov  5625  fnovim  5629  fnrnov  5666  foov  5667  funimassov  5670  ovelimab  5671  ofc12  5751  caofinvl  5753  dftpos3  5900  tfr0  5960  rdgisucinc  5995  oasuc  6067  ecinxp  6204  phplem1  6338  indpi  6532  nqnq0pi  6628  nq0m0r  6646  addnqpr1  6752  recexgt0sr  6950  recidpipr  7024  recidpirq  7026  axrnegex  7045  nntopi  7060  cnref1o  8733  fztp  9095  fseq1m1p1  9112  frecuzrdgrrn  9410  frecuzrdgsuc  9417  mulexpzap  9516  expaddzap  9520  bcp1m1  9692  cjexp  9780  rexuz3  9876  climconst  10129  eucalgval  10436  eucalginv  10438  eucalglt  10439  eucialgcvga  10440  eucialg  10441  sqpweven  10553  2sqpwodd  10554