Theorem sstrdi 3195

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

Syntax hints:   -> wi 4   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  difss2  3291  sstpr  3787  rintm  4009  eqbrrdva  4836  dmxpss2  5102  rnxpss2  5103  ssxpbm  5105  ssxp1  5106  ssxp2  5107  relfld  5198  funssxp  5427  dff2  5706  fliftf  5846  1stcof  6221  2ndcof  6222  tfrlemibfn  6386  tfr1onlembfn  6402  tfrcllemssrecs  6410  tfrcllembfn  6415  sucinc2  6504  peano5nnnn  7959  peano5nni  8993  suprzclex  9424  ioodisj  10068  fzssnn  10143  fzossnn0  10251  elfzom1elp1fzo  10278  frecuzrdgtcl  10504  frecuzrdgdomlem  10509  frecuzrdgfunlem  10511  zfz1iso  10933  seq3coll  10934  summodclem2a  11546  summodclem2  11547  zsumdc  11549  fsumsersdc  11560  fsum3cvg3  11561  prodmodclem2a  11741  prodmodclem2  11742  zproddc  11744  4sqlem11  12570  exmidunben  12643  nninfdclemp1  12667  strsetsid  12711  reldvdsrsrg  13648  lmss  14482  dvbssntrcntop  14920  dvcjbr  14944  reeff1olem  15007  peano5set  15586