Theorem sstrdi 3240

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

Hypotheses

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

Assertion

Ref	Expression
sstrdi	|- ( ph -> A C_ C )

Proof of Theorem sstrdi

Step	Hyp	Ref	Expression
1		sstrdi.1	. 2 |- ( ph -> A C_ B )
2		sstrdi.2	. . 3 |- B C_ C
3	2	a1i 9	. 2 |- ( ph -> B C_ C )
4	1, 3	sstrd 3238	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  difss2  3337  sstpr  3845  rintm  4068  eqbrrdva  4906  dmxpss2  5176  rnxpss2  5177  ssxpbm  5179  ssxp1  5180  ssxp2  5181  relfld  5272  funssxp  5512  dff2  5799  fliftf  5950  1stcof  6335  2ndcof  6336  tfrlemibfn  6537  tfr1onlembfn  6553  tfrcllemssrecs  6561  tfrcllembfn  6566  sucinc2  6657  peano5nnnn  8172  peano5nni  9205  suprzclex  9639  ioodisj  10289  fzssnn  10365  fzossnn0  10474  elfzom1elp1fzo  10510  frecuzrdgtcl  10737  frecuzrdgdomlem  10742  frecuzrdgfunlem  10744  zfz1iso  11168  seq3coll  11169  summodclem2a  12022  summodclem2  12023  zsumdc  12025  fsumsersdc  12036  fsum3cvg3  12037  prodmodclem2a  12217  prodmodclem2  12218  zproddc  12220  4sqlem11  13054  exmidunben  13127  nninfdclemp1  13151  strsetsid  13195  lmss  15057  dvbssntrcntop  15495  dvcjbr  15519  reeff1olem  15582  peano5set  16656