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  5493  dff2  5779  fliftf  5923  1stcof  6309  2ndcof  6310  tfrlemibfn  6474  tfr1onlembfn  6490  tfrcllemssrecs  6498  tfrcllembfn  6503  sucinc2  6592  peano5nnnn  8079  peano5nni  9113  suprzclex  9545  ioodisj  10189  fzssnn  10264  fzossnn0  10373  elfzom1elp1fzo  10408  frecuzrdgtcl  10634  frecuzrdgdomlem  10639  frecuzrdgfunlem  10641  zfz1iso  11063  seq3coll  11064  summodclem2a  11892  summodclem2  11893  zsumdc  11895  fsumsersdc  11906  fsum3cvg3  11907  prodmodclem2a  12087  prodmodclem2  12088  zproddc  12090  4sqlem11  12924  exmidunben  12997  nninfdclemp1  13021  strsetsid  13065  lmss  14920  dvbssntrcntop  15358  dvcjbr  15382  reeff1olem  15445  peano5set  16303