Theorem sstrd 3258

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  sstrid  3259  sstrdi  3260  rabssrabd  3335  ssdif2d  3368  tfisi  4736  funss  5399  fssxp  5558  fvmptssdm  5793  suppssov1  6302  suppssfvg  6507  tposss  6521  tfrlem1  6583  tfrlemibfn  6603  tfr1onlembfn  6619  tfr1onlemubacc  6621  tfr1onlemres  6624  tfrcllembfn  6632  tfrcllemubacc  6634  tfrcllemres  6637  ecinxp  6888  undifdc  7236  sbthlem1  7280  seqsplitg  10948  iseqf1olemnab  10960  seqf1oglem2a  10977  fiubm  11294  swrdval2  11446  isumss  12184  prodssdc  12382  ennnfoneleminc  13361  strsetsid  13444  strleund  13517  strext  13519  imasaddvallemg  13696  subsubm  13850  subsubg  14060  subgintm  14061  cntzidss  14173  gsum2dfilem2  14273  subsubrng  14632  subsubrg  14663  lssintclm  14831  lspss  14846  lspun  14849  lsslsp  14876  aspss  15129  ntrss  15357  neiint  15383  neiss  15388  restopnb  15419  iscnp4  15456  blssps  15665  blss  15666  xmettx  15748  tgqioo  15793  rescncf  15819  suplociccreex  15862  suplociccex  15863  dvbss  15923  dvbsssg  15924  dvfgg  15926  dvidsslem  15931  dvconstss  15936  dvcnp2cntop  15937  dvcn  15938  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  chtublem  16307