Theorem sstrd 3190

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 3188	. 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 3154

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 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  sstrid  3191  sstrdi  3192  ssdif2d  3299  tfisi  4620  funss  5274  fssxp  5422  fvmptssdm  5643  suppssfv  6128  suppssov1  6129  tposss  6301  tfrlem1  6363  tfrlemibfn  6383  tfr1onlembfn  6399  tfr1onlemubacc  6401  tfr1onlemres  6404  tfrcllembfn  6412  tfrcllemubacc  6414  tfrcllemres  6417  ecinxp  6666  undifdc  6982  sbthlem1  7018  seqsplitg  10563  iseqf1olemnab  10575  seqf1oglem2a  10592  fiubm  10902  isumss  11537  prodssdc  11735  ennnfoneleminc  12571  strsetsid  12654  strleund  12724  strext  12726  imasaddvallemg  12901  subsubm  13058  subsubg  13270  subgintm  13271  subsubrng  13713  subsubrg  13744  lssintclm  13883  lspss  13898  lspun  13901  lsslsp  13928  ntrss  14298  neiint  14324  neiss  14329  restopnb  14360  iscnp4  14397  blssps  14606  blss  14607  xmettx  14689  tgqioo  14734  rescncf  14760  suplociccreex  14803  suplociccex  14804  dvbss  14864  dvbsssg  14865  dvfgg  14867  dvidsslem  14872  dvconstss  14877  dvcnp2cntop  14878  dvcn  14879  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886