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  4734  funss  5396  fssxp  5555  fvmptssdm  5790  suppssov1  6299  suppssfvg  6503  tposss  6517  tfrlem1  6579  tfrlemibfn  6599  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemres  6620  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemres  6633  ecinxp  6884  undifdc  7231  sbthlem1  7274  seqsplitg  10940  iseqf1olemnab  10952  seqf1oglem2a  10969  fiubm  11286  swrdval2  11438  isumss  12176  prodssdc  12374  ennnfoneleminc  13353  strsetsid  13436  strleund  13508  strext  13510  imasaddvallemg  13687  subsubm  13841  subsubg  14051  subgintm  14052  subsubrng  14573  subsubrg  14604  lssintclm  14772  lspss  14787  lspun  14790  lsslsp  14817  aspss  15070  ntrss  15272  neiint  15298  neiss  15303  restopnb  15334  iscnp4  15371  blssps  15580  blss  15581  xmettx  15663  tgqioo  15708  rescncf  15734  suplociccreex  15777  suplociccex  15778  dvbss  15838  dvbsssg  15839  dvfgg  15841  dvidsslem  15846  dvconstss  15851  dvcnp2cntop  15852  dvcn  15853  dvaddxxbr  15854  dvmulxxbr  15855  dvcoapbr  15860  chtublem  16217