Theorem syl6eq 2401

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 10	. 2 |- (ph -> B = C)
4	1, 3	eqtrd 2385	1 |- (ph -> A = C)

Syntax hints:   -> wi 4   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  syl6req  2402  syl6eqr  2403  3eqtr3g  2408  3eqtr4a  2411  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202  un00  3587  disjssun  3609  diftpsn3  3850  intsng  3962  uniintsn  3964  rint0  3967  iinrab2  4030  riin0  4040  iununi  4051  prprc2  4123  preq12b  4128  pw10b  4167  uniabio  4350  iotanul  4355  dfiota4  4373  nnsucelr  4429  addcnnul  4454  preaddccan2  4456  ncfinraise  4482  tfin11  4494  tfindi  4497  tfinsuc  4499  tfinltfinlem1  4501  tfinltfin  4502  evenodddisj  4517  eventfin  4518  oddtfin  4519  nnadjoin  4521  nnpweq  4524  sfin01  4529  sfintfin  4533  tfinnn  4535  1cvsfin  4543  vfinncvntnn  4549  dmxpid  4925  resiima  5013  xpnz  5046  xpdisj1  5048  xpdisj2  5049  resdisj  5051  dmxpss  5053  rnxpid  5055  xpcan  5058  xpcan2  5059  dmsnopss  5068  cnvresid  5167  funcnvres2  5168  funimacnv  5169  fcoi2  5242  f1o00  5318  funfv  5376  funfv2  5377  funfv2f  5378  fvun1  5380  fvunsn  5445  fvpr1  5450  fconst5  5456  op1std  5523  op2ndd  5524  fnrnov  5606  fvmpt2i  5704  pw1fnval  5852  pw1fnf1o  5856  ecexr  5951  map0e  6024  enmap2lem3  6066  enmap2lem5  6068  ncdisjun  6137  1cnc  6140  muc0  6143  ce0nnul  6178  ce0nulnc  6185  ce2  6193  lectr  6212  leaddc1  6215  addceq0  6220  taddc  6230  letc  6232  tce2  6237  te0c  6238  ce0lenc1  6240  tlenc1c  6241  brtcfn  6247  nclenn  6250  ncslesuc  6268  nmembers1  6272  nncdiv3  6278  nnc3n3p1  6279  nchoicelem2  6291  nchoicelem7  6296  nchoicelem17  6306  frecxp  6315