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  9309  suprzclex  9748  ioodisj  10405  fzssnn  10484  fzossnn0  10594  elfzom1elp1fzo  10630  frecuzrdgtcl  10862  frecuzrdgdomlem  10867  frecuzrdgfunlem  10869  zfz1iso  11307  seq3coll  11308  summodclem2a  12164  summodclem2  12165  zsumdc  12167  fsumsersdc  12178  fsum3cvg3  12179  prodmodclem2a  12359  prodmodclem2  12360  zproddc  12362  4sqlem11  13200  ballotfilemfc0  13281  ballotfilemsima  13308  exmidunben  13366  nninfdclemp1  13390  strsetsid  13434  lmss  15396  dvbssntrcntop  15834  dvcjbr  15858  reeff1olem  15921  peano5set  17064