Theorem sstrd 3258

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

Syntax hints:   -> wi 4   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  sstrid  3259  sstrdi  3260  rabssrabd  3335  ssdif2d  3368  tfisi  4729  funss  5391  fssxp  5550  fvmptssdm  5784  suppssov1  6289  suppssfvg  6493  tposss  6507  tfrlem1  6569  tfrlemibfn  6589  tfr1onlembfn  6605  tfr1onlemubacc  6607  tfr1onlemres  6610  tfrcllembfn  6618  tfrcllemubacc  6620  tfrcllemres  6623  ecinxp  6874  undifdc  7221  sbthlem1  7264  seqsplitg  10904  iseqf1olemnab  10916  seqf1oglem2a  10933  fiubm  11249  swrdval2  11401  isumss  12136  prodssdc  12334  ennnfoneleminc  13280  strsetsid  13363  strleund  13434  strext  13436  imasaddvallemg  13613  subsubm  13767  subsubg  13977  subgintm  13978  subsubrng  14495  subsubrg  14526  lssintclm  14693  lspss  14708  lspun  14711  lsslsp  14738  ntrss  15143  neiint  15169  neiss  15174  restopnb  15205  iscnp4  15242  blssps  15451  blss  15452  xmettx  15534  tgqioo  15579  rescncf  15605  suplociccreex  15648  suplociccex  15649  dvbss  15709  dvbsssg  15710  dvfgg  15712  dvidsslem  15717  dvconstss  15722  dvcnp2cntop  15723  dvcn  15724  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731