Theorem sstrd 3112

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

Syntax hints:   → wi 4   ⊆ wss 3076

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  sstrid  3113  sstrdi  3114  ssdif2d  3220  tfisi  4509  funss  5150  fssxp  5298  fvmptssdm  5513  suppssfv  5986  suppssov1  5987  tposss  6151  tfrlem1  6213  tfrlemibfn  6233  tfr1onlembfn  6249  tfr1onlemubacc  6251  tfr1onlemres  6254  tfrcllembfn  6262  tfrcllemubacc  6264  tfrcllemres  6267  ecinxp  6512  undifdc  6820  sbthlem1  6853  iseqf1olemnab  10292  isumss  11192  ennnfoneleminc  11960  strsetsid  12031  strleund  12086  ntrss  12327  neiint  12353  neiss  12358  restopnb  12389  iscnp4  12426  blssps  12635  blss  12636  xmettx  12718  tgqioo  12755  rescncf  12776  suplociccreex  12810  suplociccex  12811  dvbss  12862  dvbsssg  12863  dvfgg  12865  dvcnp2cntop  12871  dvcn  12872  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879