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  4680  funss  5340  fssxp  5496  fvmptssdm  5724  suppssfv  6223  suppssov1  6224  tposss  6403  tfrlem1  6465  tfrlemibfn  6485  tfr1onlembfn  6501  tfr1onlemubacc  6503  tfr1onlemres  6506  tfrcllembfn  6514  tfrcllemubacc  6516  tfrcllemres  6519  ecinxp  6770  undifdc  7102  sbthlem1  7140  seqsplitg  10728  iseqf1olemnab  10740  seqf1oglem2a  10757  fiubm  11068  swrdval2  11204  isumss  11923  prodssdc  12121  ennnfoneleminc  13003  strsetsid  13086  strleund  13157  strext  13159  imasaddvallemg  13369  subsubm  13537  subsubg  13755  subgintm  13756  subsubrng  14199  subsubrg  14230  lssintclm  14369  lspss  14384  lspun  14387  lsslsp  14414  ntrss  14814  neiint  14840  neiss  14845  restopnb  14876  iscnp4  14913  blssps  15122  blss  15123  xmettx  15205  tgqioo  15250  rescncf  15276  suplociccreex  15319  suplociccex  15320  dvbss  15380  dvbsssg  15381  dvfgg  15383  dvidsslem  15388  dvconstss  15393  dvcnp2cntop  15394  dvcn  15395  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402