Theorem sstrd 3235

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 3233	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3198

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 3204  df-ss 3211

This theorem is referenced by:  sstrid  3236  sstrdi  3237  ssdif2d  3344  tfisi  4683  funss  5343  fssxp  5499  fvmptssdm  5727  suppssfv  6226  suppssov1  6227  tposss  6407  tfrlem1  6469  tfrlemibfn  6489  tfr1onlembfn  6505  tfr1onlemubacc  6507  tfr1onlemres  6510  tfrcllembfn  6518  tfrcllemubacc  6520  tfrcllemres  6523  ecinxp  6774  undifdc  7111  sbthlem1  7150  seqsplitg  10744  iseqf1olemnab  10756  seqf1oglem2a  10773  fiubm  11085  swrdval2  11225  isumss  11945  prodssdc  12143  ennnfoneleminc  13025  strsetsid  13108  strleund  13179  strext  13181  imasaddvallemg  13391  subsubm  13559  subsubg  13777  subgintm  13778  subsubrng  14221  subsubrg  14252  lssintclm  14391  lspss  14406  lspun  14409  lsslsp  14436  ntrss  14836  neiint  14862  neiss  14867  restopnb  14898  iscnp4  14935  blssps  15144  blss  15145  xmettx  15227  tgqioo  15272  rescncf  15298  suplociccreex  15341  suplociccex  15342  dvbss  15402  dvbsssg  15403  dvfgg  15405  dvidsslem  15410  dvconstss  15415  dvcnp2cntop  15416  dvcn  15417  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424