Theorem sstrd 3107

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 3105	. 2 |- ( ( A C_ B /\ B C_ C ) -> A C_ C )
4	1, 2, 3	syl2anc 408	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3071

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  sstrid  3108  sstrdi  3109  ssdif2d  3215  tfisi  4501  funss  5142  fssxp  5290  fvmptssdm  5505  suppssfv  5978  suppssov1  5979  tposss  6143  tfrlem1  6205  tfrlemibfn  6225  tfr1onlembfn  6241  tfr1onlemubacc  6243  tfr1onlemres  6246  tfrcllembfn  6254  tfrcllemubacc  6256  tfrcllemres  6259  ecinxp  6504  undifdc  6812  sbthlem1  6845  iseqf1olemnab  10261  isumss  11160  ennnfoneleminc  11924  strsetsid  11992  strleund  12047  ntrss  12288  neiint  12314  neiss  12319  restopnb  12350  iscnp4  12387  blssps  12596  blss  12597  xmettx  12679  tgqioo  12716  rescncf  12737  suplociccreex  12771  suplociccex  12772  dvbss  12823  dvbsssg  12824  dvfgg  12826  dvcnp2cntop  12832  dvcn  12833  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840