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  4950  dmxpss2  5220  rnxpss2  5221  ssxpbm  5223  ssxp1  5224  ssxp2  5225  relfld  5316  funssxp  5557  dff2  5852  fliftf  6005  1stcof  6397  2ndcof  6398  tfrlemibfn  6599  tfr1onlembfn  6615  tfrcllemssrecs  6623  tfrcllembfn  6628  sucinc2  6719  peano5nnnn  8259  peano5nni  9307  suprzclex  9744  ioodisj  10395  fzssnn  10474  fzossnn0  10584  elfzom1elp1fzo  10620  frecuzrdgtcl  10849  frecuzrdgdomlem  10854  frecuzrdgfunlem  10856  zfz1iso  11293  seq3coll  11294  summodclem2a  12148  summodclem2  12149  zsumdc  12151  fsumsersdc  12162  fsum3cvg3  12163  prodmodclem2a  12343  prodmodclem2  12344  zproddc  12346  4sqlem11  13180  ballotfilemfc0  13232  ballotfilemsima  13259  exmidunben  13317  nninfdclemp1  13341  strsetsid  13385  lmss  15347  dvbssntrcntop  15785  dvcjbr  15809  reeff1olem  15872  peano5set  16966