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 )

This proof depends on syntax axioms:   -> wi 4   C_ wss 3220

This proof depends on 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 proof 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 used by:  sstrid  3259  sstrdi  3260  rabssrabd  3335  ssdif2d  3368  tfisi  4734  funss  5396  fssxp  5555  fvmptssdm  5790  suppssov1  6299  suppssfvg  6503  tposss  6517  tfrlem1  6579  tfrlemibfn  6599  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemres  6620  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemres  6633  ecinxp  6884  undifdc  7231  sbthlem1  7274  seqsplitg  10926  iseqf1olemnab  10938  seqf1oglem2a  10955  fiubm  11271  swrdval2  11423  isumss  12158  prodssdc  12356  ennnfoneleminc  13302  strsetsid  13385  strleund  13457  strext  13459  imasaddvallemg  13636  subsubm  13790  subsubg  14000  subgintm  14001  subsubrng  14522  subsubrg  14553  lssintclm  14721  lspss  14736  lspun  14739  lsslsp  14766  aspss  15019  ntrss  15220  neiint  15246  neiss  15251  restopnb  15282  iscnp4  15319  blssps  15528  blss  15529  xmettx  15611  tgqioo  15656  rescncf  15682  suplociccreex  15725  suplociccex  15726  dvbss  15786  dvbsssg  15787  dvfgg  15789  dvidsslem  15794  dvconstss  15799  dvcnp2cntop  15800  dvcn  15801  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808