Theorem syl6ss 2110

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 2089	. 2 |- (A (_ B <-> A (_ C)
4	1, 3	sylib 198	1 |- (ph -> A (_ C)

Syntax hints:   -> wi 3   = wceq 958   (_ wss 2050

This theorem is referenced by:  syl6ssr 2111  sspr 2479  sspwuni 2764  cflecard 4924  infxpidmlem11 7563  distop 7646  elcls 7701  uniopn 7858  opnuni 7865  tgioo 7912  lmsslem 7949  dfchsup2 9293  hsupval2t 9295  hsupvalt 9296  shsupclt 9301  shsupunss 9310  shslub 9353  orthin 9365  h1datom 9499  mdslj2 10242  mdslmd1lem1 10247  fgsb 10555

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain