Theorem sstrdi 3260

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 3258	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  difss2  3357  sstpr  3877  rintm  4100  eqbrrdva  4945  dmxpss2  5215  rnxpss2  5216  ssxpbm  5218  ssxp1  5219  ssxp2  5220  relfld  5311  funssxp  5552  dff2  5843  fliftf  5995  1stcof  6387  2ndcof  6388  tfrlemibfn  6589  tfr1onlembfn  6605  tfrcllemssrecs  6613  tfrcllembfn  6618  sucinc2  6709  peano5nnnn  8249  peano5nni  9286  suprzclex  9723  ioodisj  10374  fzssnn  10452  fzossnn0  10562  elfzom1elp1fzo  10598  frecuzrdgtcl  10827  frecuzrdgdomlem  10832  frecuzrdgfunlem  10834  zfz1iso  11271  seq3coll  11272  summodclem2a  12126  summodclem2  12127  zsumdc  12129  fsumsersdc  12140  fsum3cvg3  12141  prodmodclem2a  12321  prodmodclem2  12322  zproddc  12324  4sqlem11  13158  ballotfilemfc0  13210  ballotfilemsima  13237  exmidunben  13295  nninfdclemp1  13319  strsetsid  13363  lmss  15270  dvbssntrcntop  15708  dvcjbr  15732  reeff1olem  15795  peano5set  16880