Theorem sstrd 3138

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

Syntax hints:   → wi 4   ⊆ wss 3102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  sstrid  3139  sstrdi  3140  ssdif2d  3246  tfisi  4544  funss  5186  fssxp  5334  fvmptssdm  5549  suppssfv  6022  suppssov1  6023  tposss  6187  tfrlem1  6249  tfrlemibfn  6269  tfr1onlembfn  6285  tfr1onlemubacc  6287  tfr1onlemres  6290  tfrcllembfn  6298  tfrcllemubacc  6300  tfrcllemres  6303  ecinxp  6548  undifdc  6861  sbthlem1  6894  iseqf1olemnab  10369  isumss  11270  prodssdc  11468  ennnfoneleminc  12112  strsetsid  12183  strleund  12238  ntrss  12479  neiint  12505  neiss  12510  restopnb  12541  iscnp4  12578  blssps  12787  blss  12788  xmettx  12870  tgqioo  12907  rescncf  12928  suplociccreex  12962  suplociccex  12963  dvbss  13014  dvbsssg  13015  dvfgg  13017  dvcnp2cntop  13023  dvcn  13024  dvaddxxbr  13025  dvmulxxbr  13026  dvcoapbr  13031