Theorem syl6eq 2137

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

Syntax hints:   -> wi 4   = wceq 1290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ext 2071

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

This theorem is referenced by:  syl6req  2138  syl6eqr  2139  3eqtr3g  2144  3eqtr4a  2147  cbvralcsf  2991  cbvrexcsf  2992  cbvreucsf  2993  cbvrabcsf  2994  csbprc  3332  un00  3333  disjssun  3350  disjpr2  3510  tppreq3  3549  diftpsn3  3584  preq12b  3620  intsng  3728  uniintsnr  3730  rint0  3733  riin0  3807  iununir  3818  intexr  3992  sucprc  4248  op1stbg  4314  elreldm  4674  xpeq0r  4867  xpdisj1  4868  xpdisj2  4869  resdisj  4872  xpima1  4890  xpima2m  4891  elxp4  4931  unixp0im  4980  uniabio  5003  iotass  5010  cnvresid  5101  funimacnv  5103  f1o00  5301  dffv4g  5315  fnrnfv  5364  feqresmpt  5371  dffn5imf  5372  funfvdm2f  5382  fvun1  5383  fvmpt2  5399  fndmin  5420  fmptcof  5479  fmptcos  5480  fvunsng  5505  fvpr1  5515  fnrnov  5804  offval  5877  ofrfval  5878  op1std  5933  op2ndd  5934  fmpt2co  5995  tpostpos  6043  tfr0  6102  rdgival  6161  frec0g  6176  2oconcl  6217  om0  6233  oei0  6234  oasuc  6239  omv2  6240  nnm0r  6254  uniqs2  6366  en1  6570  en1bg  6571  fundmen  6577  mapsnen  6582  xpsnen  6591  xpcomco  6596  xpdom2  6601  xpmapenlem  6619  unsnfidcex  6684  fiintim  6693  ssfirab  6697  sbthlemi8  6727  djudom  6836  en2other2  6876  exmidfodomrlemim  6881  nq0m0r  7069  addpinq1  7077  genipv  7122  genpelvl  7125  genpelvu  7126  cauappcvgprlem1  7272  caucvgsrlemoffres  7399  addresr  7428  mulresr  7429  axcnre  7470  add20  8006  rimul  8116  rereim  8117  mulreim  8135  fv0p1e1  8591  div4p1lem1div2  8723  nnm1nn0  8768  znegcl  8835  peano2z  8840  nneoor  8902  nn0ind-raph  8917  xnegneg  9349  xltnegi  9351  fzo0to2pr  9683  fldiv4p1lem1div2  9766  mulp1mod1  9826  frecfzennn  9887  iseqf1olemqk  9977  exp0  10013  expp1  10016  expnegap0  10017  1exp  10038  mulexp  10048  m1expeven  10056  sq0i  10100  bernneq  10128  facp1  10192  faclbnd3  10205  facubnd  10207  ibcval5  10225  hashinfom  10240  hashsng  10260  hashxp  10288  resunimafz0  10290  zfz1iso  10300  imre  10339  reim0b  10350  rereb  10351  resqrexlemover  10497  resqrexlemcalc1  10501  abs00bd  10553  maxabslemlub  10694  climconst  10732  isumz  10835  fsumf1o  10836  fsumcllem  10847  fsumadd  10854  fsumxp  10884  fsumcnv  10885  fsummulc2  10896  fsumconst  10902  fsumabs  10913  telfsumo  10914  fsumparts  10918  fsumrelem  10919  fsumiun  10925  binomlem  10931  binom  10932  binom11  10934  isumsplit  10939  arisum  10946  arisum2  10947  trireciplem  10948  georeclim  10961  cvgratnnlemseq  10974  ef0lem  11004  ege2le3  11015  efaddlem  11018  efcan  11020  eft0val  11037  ef4p  11038  efgt1p2  11039  efi4p  11062  sincossq  11093  cos2tsin  11096  absefi  11112  demoivreALT  11117  dvdsabseq  11180  odd2np1lem  11204  oddp1even  11208  opoe  11227  m1expo  11232  m1exp1  11233  nn0o1gt2  11237  gcddvds  11287  gcdcl  11290  gcdeq0  11300  gcd0id  11302  bezoutr1  11354  eucalg  11373  lcm0val  11379  lcmid  11394  rpmul  11412  dfphi2  11528  phiprmpw  11530  hashgcdeq  11536  setsresg  11586  strle1g  11638  restid2  11715  tgval2  11805  tgidm  11828  epttop  11844  ex-ceil  11919  bj-intexr  12065  peano3nninf  12163  nninfall  12166