Theorem sstrd 3102

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

Syntax hints:   → wi 4   ⊆ wss 3066

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  sstrid  3103  sstrdi  3104  ssdif2d  3210  tfisi  4496  funss  5137  fssxp  5285  fvmptssdm  5498  suppssfv  5971  suppssov1  5972  tposss  6136  tfrlem1  6198  tfrlemibfn  6218  tfr1onlembfn  6234  tfr1onlemubacc  6236  tfr1onlemres  6239  tfrcllembfn  6247  tfrcllemubacc  6249  tfrcllemres  6252  ecinxp  6497  undifdc  6805  sbthlem1  6838  iseqf1olemnab  10254  isumss  11153  ennnfoneleminc  11913  strsetsid  11981  strleund  12036  ntrss  12277  neiint  12303  neiss  12308  restopnb  12339  iscnp4  12376  blssps  12585  blss  12586  xmettx  12668  tgqioo  12705  rescncf  12726  suplociccreex  12760  suplociccex  12761  dvbss  12812  dvbsssg  12813  dvfgg  12815  dvcnp2cntop  12821  dvcn  12822  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829