Theorem syl6eq 2401

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

Hypotheses

Ref	Expression
syl6eq.1	⊢ (φ → A = B)
syl6eq.2	⊢ B = C

Assertion

Ref	Expression
syl6eq	⊢ (φ → A = C)

Proof of Theorem syl6eq

Step	Hyp	Ref	Expression
1		syl6eq.1	. 2 ⊢ (φ → A = B)
2		syl6eq.2	. . 3 ⊢ B = C
3	2	a1i 10	. 2 ⊢ (φ → B = C)
4	1, 3	eqtrd 2385	1 ⊢ (φ → 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  3198  cbvreucsf  3200  cbvrabcsf  3201  un00  3586  disjssun  3608  diftpsn3  3849  intsng  3961  uniintsn  3963  rint0  3966  iinrab2  4029  riin0  4039  iununi  4050  prprc2  4122  preq12b  4127  pw10b  4166  uniabio  4349  iotanul  4354  dfiota4  4372  nnsucelr  4428  addcnnul  4453  preaddccan2  4455  ncfinraise  4481  tfin11  4493  tfindi  4496  tfinsuc  4498  tfinltfinlem1  4500  tfinltfin  4501  evenodddisj  4516  eventfin  4517  oddtfin  4518  nnadjoin  4520  nnpweq  4523  sfin01  4528  sfintfin  4532  tfinnn  4534  1cvsfin  4542  vfinncvntnn  4548  dmxpid  4924  resiima  5012  xpnz  5045  xpdisj1  5047  xpdisj2  5048  resdisj  5050  dmxpss  5052  rnxpid  5054  xpcan  5057  xpcan2  5058  dmsnopss  5067  cnvresid  5166  funcnvres2  5167  funimacnv  5168  fcoi2  5241  f1o00  5317  funfv  5375  funfv2  5376  funfv2f  5377  fvun1  5379  fvunsn  5444  fvpr1  5449  fconst5  5455  op1std  5522  op2ndd  5523  fnrnov  5605  fvmpt2i  5703  pw1fnval  5851  pw1fnf1o  5855  ecexr  5950  map0e  6023  enmap2lem3  6065  enmap2lem5  6067  ncdisjun  6136  1cnc  6139  muc0  6142  ce0nnul  6177  ce0nulnc  6184  ce2  6192  lectr  6211  leaddc1  6214  addceq0  6219  taddc  6229  letc  6231  tce2  6236  te0c  6237  ce0lenc1  6239  tlenc1c  6240  brtcfn  6246  nclenn  6249  ncslesuc  6267  nmembers1  6271  nncdiv3  6277  nnc3n3p1  6278  nchoicelem2  6290  nchoicelem7  6295  nchoicelem17  6305  frecxp  6314