Theorem sstrdi 3260

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

This proof depends on syntax axioms:   -> wi 4   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  difss2  3357  sstpr  3882  rintm  4105  eqbrrdva  4952  dmxpss2  5223  rnxpss2  5224  ssxpbm  5226  ssxp1  5227  ssxp2  5228  relfld  5319  funssxp  5560  dff2  5855  fliftf  6008  1stcof  6401  2ndcof  6402  tfrlemibfn  6604  tfr1onlembfn  6620  tfrcllemssrecs  6628  tfrcllembfn  6633  sucinc2  6724  peano5nnnn  8265  peano5nni  9316  suprzclex  9754  ioodisj  10411  fzssnn  10490  fzossnn0  10600  elfzom1elp1fzo  10636  frecuzrdgtcl  10869  frecuzrdgdomlem  10874  frecuzrdgfunlem  10876  zfz1iso  11314  seq3coll  11315  summodclem2a  12172  summodclem2  12173  zsumdc  12175  fsumsersdc  12186  fsum3cvg3  12187  prodmodclem2a  12367  prodmodclem2  12368  zproddc  12370  4sqlem11  13208  ballotfilemfc0  13289  ballotfilemsima  13316  exmidunben  13374  nninfdclemp1  13398  strsetsid  13442  cntzidss  14171  cntzmhm2  14173  lmss  15489  dvbssntrcntop  15927  dvcjbr  15951  reeff1olem  16014  peano5set  17188