Theorem syl6eq 1140

Description: An equality transitivity deduction.

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 7	. 2 ⊢ (φ → B = C)
4	1, 3	eqtrd 1128	1 ⊢ (φ → A = C)

Syntax hints:   → wi 2   = wceq 1091

This theorem is referenced by:  syl6req 1141  syl6eqr 1142  3eqtr3g 1146  birabrdv 1648  ssin 1659  un00 1728  preq12b 1874  euuni 1954  intex 1986  bm2.5ii 2274  sucprc 2297  onuninsuc 2356  dmsnop 2547  dmxpid 2553  elreldm 2554  imasn 2616  xpdisj1 2653  xpdisj2 2654  resdisj 2656  funimacnv 2711  fconst 2774  f1o00 2823  fvprc 2829  funfv 2862  fvopabn 2873  isoid 2933  tz7.44-2 2967  rdgval 2978  1stval 3089  2ndval 3090  1st2val 3097  om0 3125  om0x 3126  oe0m 3127  oe0m0 3128  oe0 3130  om0r 3142  oe1m 3147  oawordeulem 3156  oa00 3161  nnmsucr 3182  ecoprcom 3255  ecoprass 3256  ecoprdi 3257  map0e 3266  en1 3331  fundmen 3333  mapsnen 3334  xpsnen 3339  xpcomen 3343  xpdom2 3345  sbthlem5 3353  sbthlem8 3356  mapdom2lem 3388  xpmapenlem2 3392  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  fiint 3445  inf3lema 3460  inf3lemd 3463  r1val1 3502  rankval2 3514  rankr1 3518  scott0 3542  aceq5lem3 3560  kmlem2 3581  kmlem10 3589  numthlem 3598  zornlem1 3603  fodomb 3615  cardval 3633  cardsn 3640  unxpdomlem 3649  cardcard 3655  cardiun 3665  cardaleph 3690  cardcf 3706  cfom 3710  recmulpq 3864  genpv 3896  genpass 3906  addcompr 3917  mulcompr 3919  mulcmpblnrlem 3976  recexsrlem 4006  ssgt0sr 4011  addresr 4050  mulresr 4051  ax1id 4077  axcnre 4087  addcan 4120  negeu 4124  subeq0 4163  mulcan 4207  mul0or 4210  receu 4215  add20 4329  nn0addclt 4551  nn0mulcl 4553  znegclt 4588  elnn0nn 4593  zltp1let 4597  uzind 4603  nn0ind 4612  seqlem1 4662  seqsuclem 4669  0expt 4680  1expt 4681  discrlem3 4715  nneo 4719  reim0 4809  rere 4810  abs00 4839  facp1t 4873  clim0 4882  xpnnen 4927  infxpidmlem4 4936  infxpidmlem8 4940  infxpidmlem10 4942  infmap2 4953  hvmul0t 5004  hvsubidt 5005  hvsubeq0 5035  hvsub0t 5041  hizer2t 5055  orthcom 5061  bcseq 5073  normgt0t 5078  normpyth 5090  hlim0 5140  hsn0elch 5155  ocsh 5164  occllem7 5186  pjthlem13 5237  omlsilem 5249  pjoc1 5268  shjcomt 5331  chj00 5408  h1de2b 5459  h1datom 5483  pjssge0 5573  pjsdi2 5627  pjclem1 5649  strlem3a 5693  strlem4 5695  golem1 5704  stcltrlem1 5709  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org