Theorem syl6eq 2129

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

Hypotheses

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

Assertion

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

Proof of Theorem syl6eq

Step	Hyp	Ref	Expression
1		syl6eq.1	. 2 |- ( ph -> A = B )
2		syl6eq.2	. . 3 |- B = C
3	2	a1i 9	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2113	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:  syl6req  2130  syl6eqr  2131  3eqtr3g  2136  3eqtr4a  2139  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  csbprc  3289  un00  3290  disjssun  3307  disjpr2  3456  tppreq3  3495  diftpsn3  3527  preq12b  3562  intsng  3670  uniintsnr  3672  rint0  3675  riin0  3749  iununir  3759  intexr  3925  sucprc  4167  op1stbg  4228  elreldm  4578  xpeq0r  4766  xpdisj1  4767  xpdisj2  4768  resdisj  4771  xpima1  4787  xpima2m  4788  elxp4  4828  unixp0im  4874  uniabio  4897  iotass  4904  cnvresid  4993  funimacnv  4995  f1o00  5181  dffv4g  5195  fnrnfv  5241  feqresmpt  5248  dffn5imf  5249  funfvdm2f  5259  fvun1  5260  fvmpt2  5275  fndmin  5295  fmptcof  5352  fmptcos  5353  fvunsng  5378  fvpr1  5386  fnrnov  5666  offval  5739  ofrfval  5740  op1std  5795  op2ndd  5796  fmpt2co  5857  tpostpos  5902  rdgival  5992  frec0g  6006  2oconcl  6045  om0  6061  oei0  6062  oasuc  6067  omv2  6068  nnm0r  6081  uniqs2  6189  en1  6302  en1bg  6303  fundmen  6309  xpsnen  6318  xpcomco  6323  xpdom2  6328  unsnfidcex  6385  nq0m0r  6646  addpinq1  6654  genipv  6699  genpelvl  6702  genpelvu  6703  cauappcvgprlem1  6849  caucvgsrlemoffres  6976  addresr  7005  mulresr  7006  axcnre  7047  add20  7578  rimul  7685  rereim  7686  mulreim  7704  div4p1lem1div2  8284  nnm1nn0  8329  znegcl  8382  peano2z  8387  nneoor  8449  nn0ind-raph  8464  xnegneg  8900  xltnegi  8902  fzo0to2pr  9227  fldiv4p1lem1div2  9307  mulp1mod1  9367  frecfzennn  9419  exp0  9480  expp1  9483  expnegap0  9484  1exp  9505  mulexp  9515  m1expeven  9523  sq0i  9567  bernneq  9593  facp1  9657  faclbnd3  9670  facubnd  9672  ibcval5  9690  imre  9738  reim0b  9749  rereb  9750  resqrexlemover  9896  resqrexlemcalc1  9900  abs00bd  9952  maxabslemlub  10093  climconst  10129  dvdsabseq  10247  odd2np1lem  10271  oddp1even  10275  opoe  10295  m1expo  10300  m1exp1  10301  nn0o1gt2  10305  gcddvds  10355  gcdcl  10358  gcdeq0  10368  gcd0id  10370  bezoutr1  10422  eucialg  10441  lcm0val  10447  lcmid  10462  rpmul  10480  ex-ceil  10564  bj-intexr  10699