Theorem sstrdi 3250

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

Syntax hints:   -> wi 4   C_ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  difss2  3347  sstpr  3861  rintm  4084  eqbrrdva  4925  dmxpss2  5195  rnxpss2  5196  ssxpbm  5198  ssxp1  5199  ssxp2  5200  relfld  5291  funssxp  5532  dff2  5821  fliftf  5972  1stcof  6357  2ndcof  6358  tfrlemibfn  6559  tfr1onlembfn  6575  tfrcllemssrecs  6583  tfrcllembfn  6588  sucinc2  6679  peano5nnnn  8207  peano5nni  9240  suprzclex  9676  ioodisj  10326  fzssnn  10402  fzossnn0  10511  elfzom1elp1fzo  10547  frecuzrdgtcl  10774  frecuzrdgdomlem  10779  frecuzrdgfunlem  10781  zfz1iso  11213  seq3coll  11214  summodclem2a  12067  summodclem2  12068  zsumdc  12070  fsumsersdc  12081  fsum3cvg3  12082  prodmodclem2a  12262  prodmodclem2  12263  zproddc  12265  4sqlem11  13099  exmidunben  13177  nninfdclemp1  13201  strsetsid  13245  lmss  15111  dvbssntrcntop  15549  dvcjbr  15573  reeff1olem  15636  peano5set  16710