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  10928  iseqf1olemnab  10940  seqf1oglem2a  10957  fiubm  11273  swrdval2  11425  isumss  12160  prodssdc  12358  ennnfoneleminc  13304  strsetsid  13387  strleund  13459  strext  13461  imasaddvallemg  13638  subsubm  13792  subsubg  14002  subgintm  14003  subsubrng  14524  subsubrg  14555  lssintclm  14723  lspss  14738  lspun  14741  lsslsp  14768  aspss  15021  ntrss  15222  neiint  15248  neiss  15253  restopnb  15284  iscnp4  15321  blssps  15530  blss  15531  xmettx  15613  tgqioo  15658  rescncf  15684  suplociccreex  15727  suplociccex  15728  dvbss  15788  dvbsssg  15789  dvfgg  15791  dvidsslem  15796  dvconstss  15801  dvcnp2cntop  15802  dvcn  15803  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810