Theorem sstrd 3157

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

Syntax hints:   → wi 4   ⊆ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  sstrid  3158  sstrdi  3159  ssdif2d  3266  tfisi  4571  funss  5217  fssxp  5365  fvmptssdm  5580  suppssfv  6057  suppssov1  6058  tposss  6225  tfrlem1  6287  tfrlemibfn  6307  tfr1onlembfn  6323  tfr1onlemubacc  6325  tfr1onlemres  6328  tfrcllembfn  6336  tfrcllemubacc  6338  tfrcllemres  6341  ecinxp  6588  undifdc  6901  sbthlem1  6934  iseqf1olemnab  10444  fiubm  10763  isumss  11354  prodssdc  11552  ennnfoneleminc  12366  strsetsid  12449  strleund  12506  ntrss  12913  neiint  12939  neiss  12944  restopnb  12975  iscnp4  13012  blssps  13221  blss  13222  xmettx  13304  tgqioo  13341  rescncf  13362  suplociccreex  13396  suplociccex  13397  dvbss  13448  dvbsssg  13449  dvfgg  13451  dvcnp2cntop  13457  dvcn  13458  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465