Theorem sstrd 3166

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

Syntax hints:   → wi 4   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  sstrid  3167  sstrdi  3168  ssdif2d  3275  tfisi  4587  funss  5236  fssxp  5384  fvmptssdm  5601  suppssfv  6079  suppssov1  6080  tposss  6247  tfrlem1  6309  tfrlemibfn  6329  tfr1onlembfn  6345  tfr1onlemubacc  6347  tfr1onlemres  6350  tfrcllembfn  6358  tfrcllemubacc  6360  tfrcllemres  6363  ecinxp  6610  undifdc  6923  sbthlem1  6956  iseqf1olemnab  10488  fiubm  10808  isumss  11399  prodssdc  11597  ennnfoneleminc  12412  strsetsid  12495  strleund  12562  strext  12564  imasaddvallemg  12736  subsubg  13057  subgintm  13058  subsubrg  13366  ntrss  13622  neiint  13648  neiss  13653  restopnb  13684  iscnp4  13721  blssps  13930  blss  13931  xmettx  14013  tgqioo  14050  rescncf  14071  suplociccreex  14105  suplociccex  14106  dvbss  14157  dvbsssg  14158  dvfgg  14160  dvcnp2cntop  14166  dvcn  14167  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174