Theorem sstrd 3194

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

Syntax hints:   → wi 4   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sstrid  3195  sstrdi  3196  ssdif2d  3303  tfisi  4624  funss  5278  fssxp  5428  fvmptssdm  5649  suppssfv  6135  suppssov1  6136  tposss  6313  tfrlem1  6375  tfrlemibfn  6395  tfr1onlembfn  6411  tfr1onlemubacc  6413  tfr1onlemres  6416  tfrcllembfn  6424  tfrcllemubacc  6426  tfrcllemres  6429  ecinxp  6678  undifdc  6994  sbthlem1  7032  seqsplitg  10600  iseqf1olemnab  10612  seqf1oglem2a  10629  fiubm  10939  isumss  11575  prodssdc  11773  ennnfoneleminc  12655  strsetsid  12738  strleund  12808  strext  12810  imasaddvallemg  13019  subsubm  13187  subsubg  13405  subgintm  13406  subsubrng  13848  subsubrg  13879  lssintclm  14018  lspss  14033  lspun  14036  lsslsp  14063  ntrss  14463  neiint  14489  neiss  14494  restopnb  14525  iscnp4  14562  blssps  14771  blss  14772  xmettx  14854  tgqioo  14899  rescncf  14925  suplociccreex  14968  suplociccex  14969  dvbss  15029  dvbsssg  15030  dvfgg  15032  dvidsslem  15037  dvconstss  15042  dvcnp2cntop  15043  dvcn  15044  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051