Theorem syl6eq 2088

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 2072	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  syl6req  2089  syl6eqr  2090  3eqtr3g  2095  3eqtr4a  2098  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  csbprc  3262  un00  3263  disjssun  3285  disjpr2  3434  tppreq3  3473  diftpsn3  3505  preq12b  3541  intsng  3649  uniintsnr  3651  rint0  3654  riin0  3728  iununir  3738  intexr  3904  sucprc  4149  op1stbg  4210  elreldm  4560  xpeq0r  4746  xpdisj1  4747  xpdisj2  4748  resdisj  4751  xpima1  4767  xpima2m  4768  elxp4  4808  unixp0im  4854  uniabio  4877  iotass  4884  cnvresid  4973  funimacnv  4975  f1o00  5161  dffv4g  5175  fnrnfv  5220  feqresmpt  5227  dffn5imf  5228  funfvdm2f  5238  fvun1  5239  fvmpt2  5254  fndmin  5274  fmptcof  5331  fmptcos  5332  fvunsng  5357  fvpr1  5365  fnrnov  5646  offval  5719  ofrfval  5720  op1std  5775  op2ndd  5776  fmpt2co  5837  tpostpos  5879  rdgival  5969  frec0g  5983  2oconcl  6022  om0  6038  oei0  6039  oasuc  6044  omv2  6045  nnm0r  6058  uniqs2  6166  en1  6279  en1bg  6280  fundmen  6286  xpsnen  6295  xpcomco  6300  xpdom2  6305  nq0m0r  6554  addpinq1  6562  genipv  6607  genpelvl  6610  genpelvu  6611  cauappcvgprlem1  6757  caucvgsrlemoffres  6884  addresr  6913  mulresr  6914  axcnre  6955  add20  7469  rimul  7576  rereim  7577  mulreim  7595  div4p1lem1div2  8177  nnm1nn0  8223  znegcl  8276  peano2z  8281  nneoor  8340  nn0ind-raph  8355  xnegneg  8746  xltnegi  8748  fzo0to2pr  9074  fldiv4p1lem1div2  9147  frecfzennn  9203  exp0  9259  expp1  9262  expnegap0  9263  1exp  9284  mulexp  9294  sq0i  9345  bernneq  9369  imre  9451  reim0b  9462  rereb  9463  resqrexlemover  9608  resqrexlemcalc1  9612  abs00bd  9664  climconst  9811  ex-ceil  9896  bj-intexr  10028