Theorem syl6ss 2159

Description: A chained subclass and equality deduction.

Hypotheses

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

Assertion

Ref	Expression
syl6ss	⊢ (φ → A ⊆ C)

Proof of Theorem syl6ss

Step	Hyp	Ref	Expression
1		syl6ss.1	. 2 ⊢ (φ → A ⊆ B)
2		syl6ss.2	. . 3 ⊢ B = C
3	2	sseq2i 2138	. 2 ⊢ (A ⊆ B ↔ A ⊆ C)
4	1, 3	sylib 196	1 ⊢ (φ → A ⊆ C)

Syntax hints:   → wi 3   = wceq 992   ⊆ wss 2099

This theorem is referenced by:  syl6ssr 2160  relrelss 3618  foimacnv 3814  onfununi 4209  cflecard 5062  infxpidmlem11 7774  distop 7861  elcls 7914  uniopn2 8071  opnuni 8078  tgioo 8126  lmsslem 8163  dfchsup2 9574  hsupval2 9576  hsupval 9577  shsupcl 9582  shsupunss 9591  shslubi 9634  orthin 9646  h1datomi 9780  mdslj2i 10528  mdslmd1lem1 10533  fgsb 11082  subsubtop 11479  cptclsscpt 11489  compfipin0lem 11492  compfipin0 11493  alexsublem3 11498  subtopmetlem 11505  isnrm2 11613  extbas1 11641  filcon 11665  totbndss 11993  heiborlem11 12021  heiborlem23 12033

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105

Copyright terms: Public domain