Theorem sstrdi 3236

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

Syntax hints:   -> wi 4   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  difss2  3332  sstpr  3835  rintm  4058  eqbrrdva  4892  dmxpss2  5161  rnxpss2  5162  ssxpbm  5164  ssxp1  5165  ssxp2  5166  relfld  5257  funssxp  5495  dff2  5781  fliftf  5929  1stcof  6315  2ndcof  6316  tfrlemibfn  6480  tfr1onlembfn  6496  tfrcllemssrecs  6504  tfrcllembfn  6509  sucinc2  6600  peano5nnnn  8090  peano5nni  9124  suprzclex  9556  ioodisj  10201  fzssnn  10276  fzossnn0  10385  elfzom1elp1fzo  10420  frecuzrdgtcl  10646  frecuzrdgdomlem  10651  frecuzrdgfunlem  10653  zfz1iso  11076  seq3coll  11077  summodclem2a  11908  summodclem2  11909  zsumdc  11911  fsumsersdc  11922  fsum3cvg3  11923  prodmodclem2a  12103  prodmodclem2  12104  zproddc  12106  4sqlem11  12940  exmidunben  13013  nninfdclemp1  13037  strsetsid  13081  lmss  14936  dvbssntrcntop  15374  dvcjbr  15398  reeff1olem  15461  peano5set  16386