Theorem sstrd 3234

Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)

Hypotheses

Ref	Expression
sstrd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sstrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
sstrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrd

Step	Hyp	Ref	Expression
1		sstrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sstrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
3		sstr 3232	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ 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  4676  funss  5333  fssxp  5487  fvmptssdm  5712  suppssfv  6204  suppssov1  6205  tposss  6382  tfrlem1  6444  tfrlemibfn  6464  tfr1onlembfn  6480  tfr1onlemubacc  6482  tfr1onlemres  6485  tfrcllembfn  6493  tfrcllemubacc  6495  tfrcllemres  6498  ecinxp  6747  undifdc  7074  sbthlem1  7112  seqsplitg  10698  iseqf1olemnab  10710  seqf1oglem2a  10727  fiubm  11037  swrdval2  11169  isumss  11888  prodssdc  12086  ennnfoneleminc  12968  strsetsid  13051  strleund  13122  strext  13124  imasaddvallemg  13334  subsubm  13502  subsubg  13720  subgintm  13721  subsubrng  14163  subsubrg  14194  lssintclm  14333  lspss  14348  lspun  14351  lsslsp  14378  ntrss  14778  neiint  14804  neiss  14809  restopnb  14840  iscnp4  14877  blssps  15086  blss  15087  xmettx  15169  tgqioo  15214  rescncf  15240  suplociccreex  15283  suplociccex  15284  dvbss  15344  dvbsssg  15345  dvfgg  15347  dvidsslem  15352  dvconstss  15357  dvcnp2cntop  15358  dvcn  15359  dvaddxxbr  15360  dvmulxxbr  15361  dvcoapbr  15366