Theorem sstrdi 3192

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

Syntax hints:   -> wi 4   C_ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  difss2  3288  sstpr  3784  rintm  4006  eqbrrdva  4833  dmxpss2  5099  rnxpss2  5100  ssxpbm  5102  ssxp1  5103  ssxp2  5104  relfld  5195  funssxp  5424  dff2  5703  fliftf  5843  1stcof  6218  2ndcof  6219  tfrlemibfn  6383  tfr1onlembfn  6399  tfrcllemssrecs  6407  tfrcllembfn  6412  sucinc2  6501  peano5nnnn  7954  peano5nni  8987  suprzclex  9418  ioodisj  10062  fzssnn  10137  fzossnn0  10245  elfzom1elp1fzo  10272  frecuzrdgtcl  10486  frecuzrdgdomlem  10491  frecuzrdgfunlem  10493  zfz1iso  10915  seq3coll  10916  summodclem2a  11527  summodclem2  11528  zsumdc  11530  fsumsersdc  11541  fsum3cvg3  11542  prodmodclem2a  11722  prodmodclem2  11723  zproddc  11725  4sqlem11  12542  exmidunben  12586  nninfdclemp1  12610  strsetsid  12654  reldvdsrsrg  13591  lmss  14425  dvbssntrcntop  14863  dvcjbr  14887  reeff1olem  14947  peano5set  15502