Theorem sstrd 3234

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

Syntax hints:   → wi 4   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sstrid  3235  sstrdi  3236  ssdif2d  3343  tfisi  4679  funss  5337  fssxp  5493  fvmptssdm  5721  suppssfv  6220  suppssov1  6221  tposss  6398  tfrlem1  6460  tfrlemibfn  6480  tfr1onlembfn  6496  tfr1onlemubacc  6498  tfr1onlemres  6501  tfrcllembfn  6509  tfrcllemubacc  6511  tfrcllemres  6514  ecinxp  6765  undifdc  7094  sbthlem1  7132  seqsplitg  10719  iseqf1olemnab  10731  seqf1oglem2a  10748  fiubm  11058  swrdval2  11191  isumss  11910  prodssdc  12108  ennnfoneleminc  12990  strsetsid  13073  strleund  13144  strext  13146  imasaddvallemg  13356  subsubm  13524  subsubg  13742  subgintm  13743  subsubrng  14186  subsubrg  14217  lssintclm  14356  lspss  14371  lspun  14374  lsslsp  14401  ntrss  14801  neiint  14827  neiss  14832  restopnb  14863  iscnp4  14900  blssps  15109  blss  15110  xmettx  15192  tgqioo  15237  rescncf  15263  suplociccreex  15306  suplociccex  15307  dvbss  15367  dvbsssg  15368  dvfgg  15370  dvidsslem  15375  dvconstss  15380  dvcnp2cntop  15381  dvcn  15382  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389