Theorem sstrd 3193

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 3191	. 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 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sstrid  3194  sstrdi  3195  ssdif2d  3302  tfisi  4623  funss  5277  fssxp  5425  fvmptssdm  5646  suppssfv  6131  suppssov1  6132  tposss  6304  tfrlem1  6366  tfrlemibfn  6386  tfr1onlembfn  6402  tfr1onlemubacc  6404  tfr1onlemres  6407  tfrcllembfn  6415  tfrcllemubacc  6417  tfrcllemres  6420  ecinxp  6669  undifdc  6985  sbthlem1  7023  seqsplitg  10581  iseqf1olemnab  10593  seqf1oglem2a  10610  fiubm  10920  isumss  11556  prodssdc  11754  ennnfoneleminc  12628  strsetsid  12711  strleund  12781  strext  12783  imasaddvallemg  12958  subsubm  13115  subsubg  13327  subgintm  13328  subsubrng  13770  subsubrg  13801  lssintclm  13940  lspss  13955  lspun  13958  lsslsp  13985  ntrss  14355  neiint  14381  neiss  14386  restopnb  14417  iscnp4  14454  blssps  14663  blss  14664  xmettx  14746  tgqioo  14791  rescncf  14817  suplociccreex  14860  suplociccex  14861  dvbss  14921  dvbsssg  14922  dvfgg  14924  dvidsslem  14929  dvconstss  14934  dvcnp2cntop  14935  dvcn  14936  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943