Theorem sstrd 3180

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 3178	. 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 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  sstrid  3181  sstrdi  3182  ssdif2d  3289  tfisi  4601  funss  5250  fssxp  5398  fvmptssdm  5616  suppssfv  6097  suppssov1  6098  tposss  6265  tfrlem1  6327  tfrlemibfn  6347  tfr1onlembfn  6363  tfr1onlemubacc  6365  tfr1onlemres  6368  tfrcllembfn  6376  tfrcllemubacc  6378  tfrcllemres  6381  ecinxp  6628  undifdc  6941  sbthlem1  6974  iseqf1olemnab  10506  fiubm  10826  isumss  11417  prodssdc  11615  ennnfoneleminc  12430  strsetsid  12513  strleund  12581  strext  12583  imasaddvallemg  12758  subsubm  12901  subsubg  13102  subgintm  13103  subsubrng  13522  subsubrg  13553  lssintclm  13661  lspss  13676  lspun  13679  lsslsp  13706  ntrss  14016  neiint  14042  neiss  14047  restopnb  14078  iscnp4  14115  blssps  14324  blss  14325  xmettx  14407  tgqioo  14444  rescncf  14465  suplociccreex  14499  suplociccex  14500  dvbss  14551  dvbsssg  14552  dvfgg  14554  dvcnp2cntop  14560  dvcn  14561  dvaddxxbr  14562  dvmulxxbr  14563  dvcoapbr  14568