Theorem sstrd 3234

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 3232	. 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 3197

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 3203  df-ss 3210

This theorem is referenced by:  sstrid  3235  sstrdi  3236  ssdif2d  3343  tfisi  4678  funss  5336  fssxp  5490  fvmptssdm  5718  suppssfv  6212  suppssov1  6213  tposss  6390  tfrlem1  6452  tfrlemibfn  6472  tfr1onlembfn  6488  tfr1onlemubacc  6490  tfr1onlemres  6493  tfrcllembfn  6501  tfrcllemubacc  6503  tfrcllemres  6506  ecinxp  6755  undifdc  7082  sbthlem1  7120  seqsplitg  10706  iseqf1olemnab  10718  seqf1oglem2a  10735  fiubm  11045  swrdval2  11178  isumss  11897  prodssdc  12095  ennnfoneleminc  12977  strsetsid  13060  strleund  13131  strext  13133  imasaddvallemg  13343  subsubm  13511  subsubg  13729  subgintm  13730  subsubrng  14172  subsubrg  14203  lssintclm  14342  lspss  14357  lspun  14360  lsslsp  14387  ntrss  14787  neiint  14813  neiss  14818  restopnb  14849  iscnp4  14886  blssps  15095  blss  15096  xmettx  15178  tgqioo  15223  rescncf  15249  suplociccreex  15292  suplociccex  15293  dvbss  15353  dvbsssg  15354  dvfgg  15356  dvidsslem  15361  dvconstss  15366  dvcnp2cntop  15367  dvcn  15368  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375