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  4736  funss  5399  fssxp  5558  fvmptssdm  5793  suppssov1  6302  suppssfvg  6507  tposss  6522  tfrlem1  6584  tfrlemibfn  6604  tfr1onlembfn  6620  tfr1onlemubacc  6622  tfr1onlemres  6625  tfrcllembfn  6633  tfrcllemubacc  6635  tfrcllemres  6638  ecinxp  6889  undifdc  7237  sbthlem1  7281  seqsplitg  10946  iseqf1olemnab  10958  seqf1oglem2a  10975  fiubm  11292  swrdval2  11444  isumss  12182  prodssdc  12380  ennnfoneleminc  13359  strsetsid  13442  strleund  13515  strext  13517  imasaddvallemg  13694  subsubm  13848  subsubg  14058  subgintm  14059  cntzidss  14171  gsum2dfilem2  14271  subsubrng  14630  subsubrg  14661  lssintclm  14829  lspss  14844  lspun  14847  lsslsp  14874  aspss  15127  mplsubgfilemcl  15232  ntrss  15362  neiint  15388  neiss  15393  restopnb  15424  iscnp4  15461  blssps  15670  blss  15671  xmettx  15753  tgqioo  15798  rescncf  15824  suplociccreex  15867  suplociccex  15868  dvbss  15928  dvbsssg  15929  dvfgg  15931  dvidsslem  15936  dvconstss  15941  dvcnp2cntop  15942  dvcn  15943  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  chtublem  16312