Theorem sstrd 3235

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 3233	. 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 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sstrid  3236  sstrdi  3237  ssdif2d  3344  tfisi  4683  funss  5343  fssxp  5499  fvmptssdm  5727  suppssfv  6226  suppssov1  6227  tposss  6407  tfrlem1  6469  tfrlemibfn  6489  tfr1onlembfn  6505  tfr1onlemubacc  6507  tfr1onlemres  6510  tfrcllembfn  6518  tfrcllemubacc  6520  tfrcllemres  6523  ecinxp  6774  undifdc  7109  sbthlem1  7147  seqsplitg  10741  iseqf1olemnab  10753  seqf1oglem2a  10770  fiubm  11082  swrdval2  11222  isumss  11942  prodssdc  12140  ennnfoneleminc  13022  strsetsid  13105  strleund  13176  strext  13178  imasaddvallemg  13388  subsubm  13556  subsubg  13774  subgintm  13775  subsubrng  14218  subsubrg  14249  lssintclm  14388  lspss  14403  lspun  14406  lsslsp  14433  ntrss  14833  neiint  14859  neiss  14864  restopnb  14895  iscnp4  14932  blssps  15141  blss  15142  xmettx  15224  tgqioo  15269  rescncf  15295  suplociccreex  15338  suplociccex  15339  dvbss  15399  dvbsssg  15400  dvfgg  15402  dvidsslem  15407  dvconstss  15412  dvcnp2cntop  15413  dvcn  15414  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421