Theorem sseqtrid 3178

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 3152	. . 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 1335   C_ wss 3102

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  fssdm  5331  fndmdif  5569  fneqeql2  5573  fconst4m  5684  f1opw2  6020  ecss  6514  fopwdom  6774  ssenen  6789  phplem2  6791  fiintim  6866  casefun  7019  caseinj  7023  djufun  7038  djuinj  7040  nn0supp  9125  monoord2  10358  binom1dif  11366  cnpnei  12579  cnntri  12584  cnntr  12585  cncnp  12590  cndis  12601  txdis1cn  12638  hmeontr  12673  hmeoimaf1o  12674  dvcoapbr  13031