Theorem syl6ss 2103

Description: A chained subclass and equality deduction.

Hypotheses

Ref	Expression
syl6ss.1	|- (ph -> A (_ B)
syl6ss.2	|- B = C

Assertion

Ref	Expression
syl6ss	|- (ph -> A (_ C)

Proof of Theorem syl6ss

Step	Hyp	Ref	Expression
1		syl6ss.1	. 2 |- (ph -> A (_ B)
2		syl6ss.2	. . 3 |- B = C
3	2	sseq2i 2082	. 2 |- (A (_ B <-> A (_ C)
4	1, 3	sylib 198	1 |- (ph -> A (_ C)

Syntax hints:   -> wi 3   = wceq 954   (_ wss 2043

This theorem is referenced by:  syl6ssr 2104  sspr 2471  sspwuni 2753  cflecard 4892  ioossre 6336  infxpidmlem11 7513  distop 7599  elcls 7654  uniopn 7813  opnuni 7820  tgioo 7867  lmsslem 7903  dfchsup2 9236  hsupval2t 9238  hsupvalt 9239  shsupclt 9244  shsupunss 9253  shslub 9296  orthin 9308  h1datom 9444  mdslj2 10184  mdslmd1lem1 10189  fgsb 10480

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain