Theorem sstrdi 3205

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

Syntax hints:   -> wi 4   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  difss2  3301  sstpr  3798  rintm  4020  eqbrrdva  4848  dmxpss2  5115  rnxpss2  5116  ssxpbm  5118  ssxp1  5119  ssxp2  5120  relfld  5211  funssxp  5445  dff2  5724  fliftf  5868  1stcof  6249  2ndcof  6250  tfrlemibfn  6414  tfr1onlembfn  6430  tfrcllemssrecs  6438  tfrcllembfn  6443  sucinc2  6532  peano5nnnn  8005  peano5nni  9039  suprzclex  9471  ioodisj  10115  fzssnn  10190  fzossnn0  10299  elfzom1elp1fzo  10331  frecuzrdgtcl  10557  frecuzrdgdomlem  10562  frecuzrdgfunlem  10564  zfz1iso  10986  seq3coll  10987  summodclem2a  11692  summodclem2  11693  zsumdc  11695  fsumsersdc  11706  fsum3cvg3  11707  prodmodclem2a  11887  prodmodclem2  11888  zproddc  11890  4sqlem11  12724  exmidunben  12797  nninfdclemp1  12821  strsetsid  12865  reldvdsrsrg  13854  lmss  14718  dvbssntrcntop  15156  dvcjbr  15180  reeff1olem  15243  peano5set  15876