Theorem sstrd 3238

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

Syntax hints:   → wi 4   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sstrid  3239  sstrdi  3240  rabssrabd  3315  ssdif2d  3348  tfisi  4691  funss  5352  fssxp  5510  fvmptssdm  5740  suppssov1  6241  suppssfvg  6441  tposss  6455  tfrlem1  6517  tfrlemibfn  6537  tfr1onlembfn  6553  tfr1onlemubacc  6555  tfr1onlemres  6558  tfrcllembfn  6566  tfrcllemubacc  6568  tfrcllemres  6571  ecinxp  6822  undifdc  7159  sbthlem1  7199  seqsplitg  10795  iseqf1olemnab  10807  seqf1oglem2a  10824  fiubm  11136  swrdval2  11279  isumss  12013  prodssdc  12211  ennnfoneleminc  13093  strsetsid  13176  strleund  13247  strext  13249  imasaddvallemg  13459  subsubm  13627  subsubg  13845  subgintm  13846  subsubrng  14290  subsubrg  14321  lssintclm  14460  lspss  14475  lspun  14478  lsslsp  14505  ntrss  14910  neiint  14936  neiss  14941  restopnb  14972  iscnp4  15009  blssps  15218  blss  15219  xmettx  15301  tgqioo  15346  rescncf  15372  suplociccreex  15415  suplociccex  15416  dvbss  15476  dvbsssg  15477  dvfgg  15479  dvidsslem  15484  dvconstss  15489  dvcnp2cntop  15490  dvcn  15491  dvaddxxbr  15492  dvmulxxbr  15493  dvcoapbr  15498