Theorem sstrd 3205

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

Syntax hints:   → wi 4   ⊆ wss 3168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3174  df-ss 3181

This theorem is referenced by:  sstrid  3206  sstrdi  3207  ssdif2d  3314  tfisi  4640  funss  5296  fssxp  5450  fvmptssdm  5674  suppssfv  6164  suppssov1  6165  tposss  6342  tfrlem1  6404  tfrlemibfn  6424  tfr1onlembfn  6440  tfr1onlemubacc  6442  tfr1onlemres  6445  tfrcllembfn  6453  tfrcllemubacc  6455  tfrcllemres  6458  ecinxp  6707  undifdc  7033  sbthlem1  7071  seqsplitg  10647  iseqf1olemnab  10659  seqf1oglem2a  10676  fiubm  10986  swrdval2  11118  isumss  11752  prodssdc  11950  ennnfoneleminc  12832  strsetsid  12915  strleund  12985  strext  12987  imasaddvallemg  13197  subsubm  13365  subsubg  13583  subgintm  13584  subsubrng  14026  subsubrg  14057  lssintclm  14196  lspss  14211  lspun  14214  lsslsp  14241  ntrss  14641  neiint  14667  neiss  14672  restopnb  14703  iscnp4  14740  blssps  14949  blss  14950  xmettx  15032  tgqioo  15077  rescncf  15103  suplociccreex  15146  suplociccex  15147  dvbss  15207  dvbsssg  15208  dvfgg  15210  dvidsslem  15215  dvconstss  15220  dvcnp2cntop  15221  dvcn  15222  dvaddxxbr  15223  dvmulxxbr  15224  dvcoapbr  15229