Theorem sstrd 3237

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

Syntax hints:   → wi 4   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sstrid  3238  sstrdi  3239  ssdif2d  3346  tfisi  4685  funss  5345  fssxp  5502  fvmptssdm  5731  suppssfv  6231  suppssov1  6232  tposss  6412  tfrlem1  6474  tfrlemibfn  6494  tfr1onlembfn  6510  tfr1onlemubacc  6512  tfr1onlemres  6515  tfrcllembfn  6523  tfrcllemubacc  6525  tfrcllemres  6528  ecinxp  6779  undifdc  7116  sbthlem1  7156  seqsplitg  10752  iseqf1olemnab  10764  seqf1oglem2a  10781  fiubm  11093  swrdval2  11236  isumss  11957  prodssdc  12155  ennnfoneleminc  13037  strsetsid  13120  strleund  13191  strext  13193  imasaddvallemg  13403  subsubm  13571  subsubg  13789  subgintm  13790  subsubrng  14234  subsubrg  14265  lssintclm  14404  lspss  14419  lspun  14422  lsslsp  14449  ntrss  14849  neiint  14875  neiss  14880  restopnb  14911  iscnp4  14948  blssps  15157  blss  15158  xmettx  15240  tgqioo  15285  rescncf  15311  suplociccreex  15354  suplociccex  15355  dvbss  15415  dvbsssg  15416  dvfgg  15418  dvidsslem  15423  dvconstss  15428  dvcnp2cntop  15429  dvcn  15430  dvaddxxbr  15431  dvmulxxbr  15432  dvcoapbr  15437