Theorem syl6eq 2130

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

Hypotheses

Ref	Expression
syl6eq.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6eq.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
syl6eq	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl6eq

Step	Hyp	Ref	Expression
1		syl6eq.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6eq.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2114	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1285

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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075

This theorem is referenced by:  syl6req  2131  syl6eqr  2132  3eqtr3g  2137  3eqtr4a  2140  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  csbprc  3296  un00  3297  disjssun  3314  disjpr2  3464  tppreq3  3503  diftpsn3  3535  preq12b  3570  intsng  3678  uniintsnr  3680  rint0  3683  riin0  3757  iununir  3767  intexr  3933  sucprc  4175  op1stbg  4236  elreldm  4588  xpeq0r  4776  xpdisj1  4777  xpdisj2  4778  resdisj  4781  xpima1  4797  xpima2m  4798  elxp4  4838  unixp0im  4884  uniabio  4907  iotass  4914  cnvresid  5004  funimacnv  5006  f1o00  5192  dffv4g  5206  fnrnfv  5252  feqresmpt  5259  dffn5imf  5260  funfvdm2f  5270  fvun1  5271  fvmpt2  5286  fndmin  5306  fmptcof  5363  fmptcos  5364  fvunsng  5389  fvpr1  5397  fnrnov  5677  offval  5750  ofrfval  5751  op1std  5806  op2ndd  5807  fmpt2co  5868  tpostpos  5913  tfr0  5972  rdgival  6031  frec0g  6046  2oconcl  6086  om0  6102  oei0  6103  oasuc  6108  omv2  6109  nnm0r  6123  uniqs2  6232  en1  6346  en1bg  6347  fundmen  6353  xpsnen  6365  xpcomco  6370  xpdom2  6375  unsnfidcex  6440  en2other2  6522  nq0m0r  6708  addpinq1  6716  genipv  6761  genpelvl  6764  genpelvu  6765  cauappcvgprlem1  6911  caucvgsrlemoffres  7038  addresr  7067  mulresr  7068  axcnre  7109  add20  7645  rimul  7752  rereim  7753  mulreim  7771  div4p1lem1div2  8351  nnm1nn0  8396  znegcl  8463  peano2z  8468  nneoor  8530  nn0ind-raph  8545  xnegneg  8976  xltnegi  8978  fzo0to2pr  9304  fldiv4p1lem1div2  9387  mulp1mod1  9447  frecfzennn  9508  exp0  9577  expp1  9580  expnegap0  9581  1exp  9602  mulexp  9612  m1expeven  9620  sq0i  9664  bernneq  9690  facp1  9754  faclbnd3  9767  facubnd  9769  ibcval5  9787  sizeinf  9802  sizesng  9822  imre  9876  reim0b  9887  rereb  9888  resqrexlemover  10034  resqrexlemcalc1  10038  abs00bd  10090  maxabslemlub  10231  climconst  10267  dvdsabseq  10392  odd2np1lem  10416  oddp1even  10420  opoe  10439  m1expo  10444  m1exp1  10445  nn0o1gt2  10449  gcddvds  10499  gcdcl  10502  gcdeq0  10512  gcd0id  10514  bezoutr1  10566  eucialg  10585  lcm0val  10591  lcmid  10606  rpmul  10624  ex-ceil  10742  bj-intexr  10884