Theorem sstrd 3189

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

Syntax hints:   → wi 4   ⊆ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  sstrid  3190  sstrdi  3191  ssdif2d  3298  tfisi  4619  funss  5273  fssxp  5421  fvmptssdm  5642  suppssfv  6126  suppssov1  6127  tposss  6299  tfrlem1  6361  tfrlemibfn  6381  tfr1onlembfn  6397  tfr1onlemubacc  6399  tfr1onlemres  6402  tfrcllembfn  6410  tfrcllemubacc  6412  tfrcllemres  6415  ecinxp  6664  undifdc  6980  sbthlem1  7016  seqsplitg  10560  iseqf1olemnab  10572  seqf1oglem2a  10589  fiubm  10899  isumss  11534  prodssdc  11732  ennnfoneleminc  12568  strsetsid  12651  strleund  12721  strext  12723  imasaddvallemg  12898  subsubm  13055  subsubg  13267  subgintm  13268  subsubrng  13710  subsubrg  13741  lssintclm  13880  lspss  13895  lspun  13898  lsslsp  13925  ntrss  14287  neiint  14313  neiss  14318  restopnb  14349  iscnp4  14386  blssps  14595  blss  14596  xmettx  14678  tgqioo  14715  rescncf  14736  suplociccreex  14778  suplociccex  14779  dvbss  14839  dvbsssg  14840  dvfgg  14842  dvcnp2cntop  14848  dvcn  14849  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856