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  6603  tfr1onlembfn  6619  tfrcllemssrecs  6627  tfrcllembfn  6632  sucinc2  6723  peano5nnnn  8265  peano5nni  9316  suprzclex  9755  ioodisj  10412  fzssnn  10491  fzossnn0  10601  elfzom1elp1fzo  10637  frecuzrdgtcl  10870  frecuzrdgdomlem  10875  frecuzrdgfunlem  10877  zfz1iso  11315  seq3coll  11316  summodclem2a  12173  summodclem2  12174  zsumdc  12176  fsumsersdc  12187  fsum3cvg3  12188  prodmodclem2a  12368  prodmodclem2  12369  zproddc  12371  4sqlem11  13209  ballotfilemfc0  13290  ballotfilemsima  13317  exmidunben  13375  nninfdclemp1  13399  strsetsid  13443  cntzidss  14172  cntzmhm2  14174  lmss  15472  dvbssntrcntop  15910  dvcjbr  15934  reeff1olem  15997  peano5set  17171