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  6230  suppssov1  6231  tposss  6411  tfrlem1  6473  tfrlemibfn  6493  tfr1onlembfn  6509  tfr1onlemubacc  6511  tfr1onlemres  6514  tfrcllembfn  6522  tfrcllemubacc  6524  tfrcllemres  6527  ecinxp  6778  undifdc  7115  sbthlem1  7155  seqsplitg  10750  iseqf1olemnab  10762  seqf1oglem2a  10779  fiubm  11091  swrdval2  11231  isumss  11951  prodssdc  12149  ennnfoneleminc  13031  strsetsid  13114  strleund  13185  strext  13187  imasaddvallemg  13397  subsubm  13565  subsubg  13783  subgintm  13784  subsubrng  14227  subsubrg  14258  lssintclm  14397  lspss  14412  lspun  14415  lsslsp  14442  ntrss  14842  neiint  14868  neiss  14873  restopnb  14904  iscnp4  14941  blssps  15150  blss  15151  xmettx  15233  tgqioo  15278  rescncf  15304  suplociccreex  15347  suplociccex  15348  dvbss  15408  dvbsssg  15409  dvfgg  15411  dvidsslem  15416  dvconstss  15421  dvcnp2cntop  15422  dvcn  15423  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430