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  6521  tfrlem1  6583  tfrlemibfn  6603  tfr1onlembfn  6619  tfr1onlemubacc  6621  tfr1onlemres  6624  tfrcllembfn  6632  tfrcllemubacc  6634  tfrcllemres  6637  ecinxp  6888  undifdc  7235  sbthlem1  7279  seqsplitg  10947  iseqf1olemnab  10959  seqf1oglem2a  10976  fiubm  11293  swrdval2  11445  isumss  12183  prodssdc  12381  ennnfoneleminc  13360  strsetsid  13443  strleund  13516  strext  13518  imasaddvallemg  13695  subsubm  13849  subsubg  14059  subgintm  14060  cntzidss  14172  gsum2dfilem2  14272  subsubrng  14631  subsubrg  14662  lssintclm  14830  lspss  14845  lspun  14848  lsslsp  14875  aspss  15128  ntrss  15345  neiint  15371  neiss  15376  restopnb  15407  iscnp4  15444  blssps  15653  blss  15654  xmettx  15736  tgqioo  15781  rescncf  15807  suplociccreex  15850  suplociccex  15851  dvbss  15911  dvbsssg  15912  dvfgg  15914  dvidsslem  15919  dvconstss  15924  dvcnp2cntop  15925  dvcn  15926  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  chtublem  16295