Theorem sstrd 3237

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 3235	. 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 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sstrid  3238  sstrdi  3239  ssdif2d  3346  tfisi  4685  funss  5345  fssxp  5502  fvmptssdm  5731  suppssfv  6231  suppssov1  6232  tposss  6412  tfrlem1  6474  tfrlemibfn  6494  tfr1onlembfn  6510  tfr1onlemubacc  6512  tfr1onlemres  6515  tfrcllembfn  6523  tfrcllemubacc  6525  tfrcllemres  6528  ecinxp  6779  undifdc  7116  sbthlem1  7156  seqsplitg  10752  iseqf1olemnab  10764  seqf1oglem2a  10781  fiubm  11093  swrdval2  11236  isumss  11970  prodssdc  12168  ennnfoneleminc  13050  strsetsid  13133  strleund  13204  strext  13206  imasaddvallemg  13416  subsubm  13584  subsubg  13802  subgintm  13803  subsubrng  14247  subsubrg  14278  lssintclm  14417  lspss  14432  lspun  14435  lsslsp  14462  ntrss  14862  neiint  14888  neiss  14893  restopnb  14924  iscnp4  14961  blssps  15170  blss  15171  xmettx  15253  tgqioo  15298  rescncf  15324  suplociccreex  15367  suplociccex  15368  dvbss  15428  dvbsssg  15429  dvfgg  15431  dvidsslem  15436  dvconstss  15441  dvcnp2cntop  15442  dvcn  15443  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450