Theorem syl6eq 2085

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

Syntax hints:   -> wi 4   = wceq 1242

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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

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

This theorem is referenced by:  syl6req  2086  syl6eqr  2087  3eqtr3g  2092  3eqtr4a  2095  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  csbprc  3256  un00  3257  disjssun  3279  disjpr2  3425  tppreq3  3464  diftpsn3  3496  preq12b  3532  intsng  3640  uniintsnr  3642  rint0  3645  riin0  3719  iununir  3729  intexr  3895  sucprc  4115  op1stbg  4176  elreldm  4503  xpeq0r  4689  xpdisj1  4690  xpdisj2  4691  resdisj  4694  xpima1  4710  xpima2m  4711  elxp4  4751  unixp0im  4797  uniabio  4820  iotass  4827  cnvresid  4916  funimacnv  4918  f1o00  5104  dffv4g  5118  fnrnfv  5163  feqresmpt  5170  dffn5imf  5171  funfvdm2f  5181  fvun1  5182  fvmpt2  5197  fndmin  5217  fmptcof  5274  fmptcos  5275  fvunsng  5300  fvpr1  5308  fnrnov  5588  offval  5661  ofrfval  5662  op1std  5717  op2ndd  5718  fmpt2co  5779  tpostpos  5820  rdgival  5909  frec0g  5922  2oconcl  5961  om0  5977  oei0  5978  oasuc  5983  omv2  5984  nnm0r  5997  uniqs2  6102  en1  6215  en1bg  6216  fundmen  6222  xpsnen  6231  xpcomco  6236  xpdom2  6241  nq0m0r  6439  addpinq1  6447  genipv  6492  genpelvl  6495  genpelvu  6496  cauappcvgprlem1  6631  addresr  6734  mulresr  6735  axcnre  6765  add20  7264  rimul  7369  rereim  7370  mulreim  7388  nnm1nn0  7999  znegcl  8052  peano2z  8057  nneoor  8116  nn0ind-raph  8131  xnegneg  8516  xltnegi  8518  fzo0to2pr  8844  frecfzennn  8884  exp0  8913  expp1  8916  expnegap0  8917  1exp  8938  mulexp  8948  sq0i  8998  bernneq  9022  imre  9079  reim0b  9090  rereb  9091  abs00bd  9224  bj-intexr  9363