Theorem sstrdi 3159

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

Syntax hints:   -> wi 4   C_ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  difss2  3255  sstpr  3742  rintm  3963  eqbrrdva  4779  dmxpss2  5041  rnxpss2  5042  ssxpbm  5044  ssxp1  5045  ssxp2  5046  relfld  5137  funssxp  5365  dff2  5638  fliftf  5776  1stcof  6140  2ndcof  6141  tfrlemibfn  6305  tfr1onlembfn  6321  tfrcllemssrecs  6329  tfrcllembfn  6334  sucinc2  6423  peano5nnnn  7847  peano5nni  8874  suprzclex  9303  ioodisj  9943  fzssnn  10017  fzossnn0  10124  elfzom1elp1fzo  10151  frecuzrdgtcl  10361  frecuzrdgdomlem  10366  frecuzrdgfunlem  10368  zfz1iso  10769  seq3coll  10770  summodclem2a  11337  summodclem2  11338  zsumdc  11340  fsumsersdc  11351  fsum3cvg3  11352  prodmodclem2a  11532  prodmodclem2  11533  zproddc  11535  exmidunben  12374  nninfdclemp1  12398  strsetsid  12442  lmss  13005  dvbssntrcntop  13412  dvcjbr  13431  reeff1olem  13451  peano5set  13940