Theorem sseqtrid 3192

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
sseqtrid.1	|- B C_ A
sseqtrid.2	|- ( ph -> A = C )

Assertion

Ref	Expression
sseqtrid	|- ( ph -> B C_ C )

Proof of Theorem sseqtrid

Step	Hyp	Ref	Expression
1		sseqtrid.2	. 2 |- ( ph -> A = C )
2		sseqtrid.1	. 2 |- B C_ A
3		sseq2 3166	. . 3 |- ( A = C -> ( B C_ A <-> B C_ C ) )
4	3	biimpa 294	. 2 |- ( ( A = C /\ B C_ A ) -> B C_ C )
5	1, 2, 4	sylancl 410	1 |- ( ph -> B C_ C )

Syntax hints:   -> wi 4   = wceq 1343   C_ wss 3116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129

This theorem is referenced by:  fssdm  5352  fndmdif  5590  fneqeql2  5594  fconst4m  5705  f1opw2  6044  ecss  6542  fopwdom  6802  ssenen  6817  phplem2  6819  fiintim  6894  casefun  7050  caseinj  7054  djufun  7069  djuinj  7071  nn0supp  9166  monoord2  10412  binom1dif  11428  cnpnei  12859  cnntri  12864  cnntr  12865  cncnp  12870  cndis  12881  txdis1cn  12918  hmeontr  12953  hmeoimaf1o  12954  dvcoapbr  13311