Theorem sstrd 3258

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

Syntax hints:   → wi 4   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  sstrid  3259  sstrdi  3260  rabssrabd  3335  ssdif2d  3368  tfisi  4732  funss  5394  fssxp  5553  fvmptssdm  5787  suppssov1  6293  suppssfvg  6497  tposss  6511  tfrlem1  6573  tfrlemibfn  6593  tfr1onlembfn  6609  tfr1onlemubacc  6611  tfr1onlemres  6614  tfrcllembfn  6622  tfrcllemubacc  6624  tfrcllemres  6627  ecinxp  6878  undifdc  7225  sbthlem1  7268  seqsplitg  10909  iseqf1olemnab  10921  seqf1oglem2a  10938  fiubm  11254  swrdval2  11406  isumss  12141  prodssdc  12339  ennnfoneleminc  13285  strsetsid  13368  strleund  13440  strext  13442  imasaddvallemg  13619  subsubm  13773  subsubg  13983  subgintm  13984  subsubrng  14505  subsubrg  14536  lssintclm  14704  lspss  14719  lspun  14722  lsslsp  14749  aspss  15002  ntrss  15203  neiint  15229  neiss  15234  restopnb  15265  iscnp4  15302  blssps  15511  blss  15512  xmettx  15594  tgqioo  15639  rescncf  15665  suplociccreex  15708  suplociccex  15709  dvbss  15769  dvbsssg  15770  dvfgg  15772  dvidsslem  15777  dvconstss  15782  dvcnp2cntop  15783  dvcn  15784  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791