Theorem sstrdi 3213

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

Syntax hints:   -> wi 4   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  difss2  3309  sstpr  3811  rintm  4034  eqbrrdva  4866  dmxpss2  5134  rnxpss2  5135  ssxpbm  5137  ssxp1  5138  ssxp2  5139  relfld  5230  funssxp  5465  dff2  5747  fliftf  5891  1stcof  6272  2ndcof  6273  tfrlemibfn  6437  tfr1onlembfn  6453  tfrcllemssrecs  6461  tfrcllembfn  6466  sucinc2  6555  peano5nnnn  8040  peano5nni  9074  suprzclex  9506  ioodisj  10150  fzssnn  10225  fzossnn0  10334  elfzom1elp1fzo  10368  frecuzrdgtcl  10594  frecuzrdgdomlem  10599  frecuzrdgfunlem  10601  zfz1iso  11023  seq3coll  11024  summodclem2a  11807  summodclem2  11808  zsumdc  11810  fsumsersdc  11821  fsum3cvg3  11822  prodmodclem2a  12002  prodmodclem2  12003  zproddc  12005  4sqlem11  12839  exmidunben  12912  nninfdclemp1  12936  strsetsid  12980  reldvdsrsrg  13969  lmss  14833  dvbssntrcntop  15271  dvcjbr  15295  reeff1olem  15358  peano5set  16075