Theorem sstrd 3203

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 3201	. 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 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  sstrid  3204  sstrdi  3205  ssdif2d  3312  tfisi  4635  funss  5290  fssxp  5443  fvmptssdm  5664  suppssfv  6154  suppssov1  6155  tposss  6332  tfrlem1  6394  tfrlemibfn  6414  tfr1onlembfn  6430  tfr1onlemubacc  6432  tfr1onlemres  6435  tfrcllembfn  6443  tfrcllemubacc  6445  tfrcllemres  6448  ecinxp  6697  undifdc  7021  sbthlem1  7059  seqsplitg  10634  iseqf1olemnab  10646  seqf1oglem2a  10663  fiubm  10973  swrdval2  11104  isumss  11702  prodssdc  11900  ennnfoneleminc  12782  strsetsid  12865  strleund  12935  strext  12937  imasaddvallemg  13147  subsubm  13315  subsubg  13533  subgintm  13534  subsubrng  13976  subsubrg  14007  lssintclm  14146  lspss  14161  lspun  14164  lsslsp  14191  ntrss  14591  neiint  14617  neiss  14622  restopnb  14653  iscnp4  14690  blssps  14899  blss  14900  xmettx  14982  tgqioo  15027  rescncf  15053  suplociccreex  15096  suplociccex  15097  dvbss  15157  dvbsssg  15158  dvfgg  15160  dvidsslem  15165  dvconstss  15170  dvcnp2cntop  15171  dvcn  15172  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179