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 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220

This proof depends on 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 proof 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 used by:  sstrid  3259  sstrdi  3260  rabssrabd  3335  ssdif2d  3368  tfisi  4736  funss  5399  fssxp  5558  fvmptssdm  5793  suppssov1  6302  suppssfvg  6507  tposss  6522  tfrlem1  6584  tfrlemibfn  6604  tfr1onlembfn  6620  tfr1onlemubacc  6622  tfr1onlemres  6625  tfrcllembfn  6633  tfrcllemubacc  6635  tfrcllemres  6638  ecinxp  6889  undifdc  7237  sbthlem1  7281  seqsplitg  10947  iseqf1olemnab  10959  seqf1oglem2a  10976  fiubm  11293  swrdval2  11445  isumss  12183  prodssdc  12381  ennnfoneleminc  13360  strsetsid  13443  strleund  13516  strext  13518  imasaddvallemg  13695  subsubm  13849  subsubg  14059  subgintm  14060  cntzidss  14172  gsum2dfilem2  14272  subsubrng  14631  subsubrg  14662  lssintclm  14830  lspss  14845  lspun  14848  lsslsp  14875  aspss  15128  mplsubgfilemcl  15246  ntrss  15378  neiint  15404  neiss  15409  restopnb  15440  iscnp4  15477  blssps  15686  blss  15687  xmettx  15769  tgqioo  15814  rescncf  15840  suplociccreex  15883  suplociccex  15884  dvbss  15944  dvbsssg  15945  dvfgg  15947  dvidsslem  15952  dvconstss  15957  dvcnp2cntop  15958  dvcn  15959  dvaddxxbr  15960  dvmulxxbr  15961  dvcoapbr  15966  chtublem  16328