Theorem sstrd 3138

Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)

Hypotheses

Ref	Expression
sstrd.1	|- ( ph -> A C_ B )
sstrd.2	|- ( ph -> B C_ C )

Assertion

Ref	Expression
sstrd	|- ( ph -> A C_ C )

Proof of Theorem sstrd

Step	Hyp	Ref	Expression
1		sstrd.1	. 2 |- ( ph -> A C_ B )
2		sstrd.2	. 2 |- ( ph -> B C_ C )
3		sstr 3136	. 2 |- ( ( A C_ B /\ B C_ C ) -> A C_ C )
4	1, 2, 3	syl2anc 409	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  sstrid  3139  sstrdi  3140  ssdif2d  3246  tfisi  4545  funss  5188  fssxp  5336  fvmptssdm  5551  suppssfv  6025  suppssov1  6026  tposss  6190  tfrlem1  6252  tfrlemibfn  6272  tfr1onlembfn  6288  tfr1onlemubacc  6290  tfr1onlemres  6293  tfrcllembfn  6301  tfrcllemubacc  6303  tfrcllemres  6306  ecinxp  6552  undifdc  6865  sbthlem1  6898  iseqf1olemnab  10380  isumss  11281  prodssdc  11479  ennnfoneleminc  12123  strsetsid  12194  strleund  12249  ntrss  12490  neiint  12516  neiss  12521  restopnb  12552  iscnp4  12589  blssps  12798  blss  12799  xmettx  12881  tgqioo  12918  rescncf  12939  suplociccreex  12973  suplociccex  12974  dvbss  13025  dvbsssg  13026  dvfgg  13028  dvcnp2cntop  13034  dvcn  13035  dvaddxxbr  13036  dvmulxxbr  13037  dvcoapbr  13042