Theorem sstrd 3238

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

Syntax hints:   -> wi 4   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sstrid  3239  sstrdi  3240  rabssrabd  3315  ssdif2d  3348  tfisi  4691  funss  5352  fssxp  5510  fvmptssdm  5740  suppssov1  6241  suppssfvg  6441  tposss  6455  tfrlem1  6517  tfrlemibfn  6537  tfr1onlembfn  6553  tfr1onlemubacc  6555  tfr1onlemres  6558  tfrcllembfn  6566  tfrcllemubacc  6568  tfrcllemres  6571  ecinxp  6822  undifdc  7159  sbthlem1  7199  seqsplitg  10797  iseqf1olemnab  10809  seqf1oglem2a  10826  fiubm  11138  swrdval2  11281  isumss  12015  prodssdc  12213  ennnfoneleminc  13095  strsetsid  13178  strleund  13249  strext  13251  imasaddvallemg  13461  subsubm  13629  subsubg  13847  subgintm  13848  subsubrng  14292  subsubrg  14323  lssintclm  14463  lspss  14478  lspun  14481  lsslsp  14508  ntrss  14913  neiint  14939  neiss  14944  restopnb  14975  iscnp4  15012  blssps  15221  blss  15222  xmettx  15304  tgqioo  15349  rescncf  15375  suplociccreex  15418  suplociccex  15419  dvbss  15479  dvbsssg  15480  dvfgg  15482  dvidsslem  15487  dvconstss  15492  dvcnp2cntop  15493  dvcn  15494  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501