Theorem sstrd 3158

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 3156	. 2 |- ( ( A C_ B /\ B C_ C ) -> A C_ C )
4	1, 2, 3	syl2anc 409	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-11 1500  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-in 3128  df-ss 3135

This theorem is referenced by:  sstrid  3159  sstrdi  3160  ssdif2d  3267  tfisi  4572  funss  5219  fssxp  5367  fvmptssdm  5584  suppssfv  6061  suppssov1  6062  tposss  6229  tfrlem1  6291  tfrlemibfn  6311  tfr1onlembfn  6327  tfr1onlemubacc  6329  tfr1onlemres  6332  tfrcllembfn  6340  tfrcllemubacc  6342  tfrcllemres  6345  ecinxp  6592  undifdc  6905  sbthlem1  6938  iseqf1olemnab  10448  fiubm  10767  isumss  11358  prodssdc  11556  ennnfoneleminc  12370  strsetsid  12453  strleund  12510  ntrss  12998  neiint  13024  neiss  13029  restopnb  13060  iscnp4  13097  blssps  13306  blss  13307  xmettx  13389  tgqioo  13426  rescncf  13447  suplociccreex  13481  suplociccex  13482  dvbss  13533  dvbsssg  13534  dvfgg  13536  dvcnp2cntop  13542  dvcn  13543  dvaddxxbr  13544  dvmulxxbr  13545  dvcoapbr  13550