Theorem sstrd 3235

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

Syntax hints:   → wi 4   ⊆ wss 3198

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 3204  df-ss 3211

This theorem is referenced by:  sstrid  3236  sstrdi  3237  ssdif2d  3344  tfisi  4681  funss  5341  fssxp  5497  fvmptssdm  5725  suppssfv  6224  suppssov1  6225  tposss  6405  tfrlem1  6467  tfrlemibfn  6487  tfr1onlembfn  6503  tfr1onlemubacc  6505  tfr1onlemres  6508  tfrcllembfn  6516  tfrcllemubacc  6518  tfrcllemres  6521  ecinxp  6772  undifdc  7107  sbthlem1  7145  seqsplitg  10739  iseqf1olemnab  10751  seqf1oglem2a  10768  fiubm  11079  swrdval2  11219  isumss  11939  prodssdc  12137  ennnfoneleminc  13019  strsetsid  13102  strleund  13173  strext  13175  imasaddvallemg  13385  subsubm  13553  subsubg  13771  subgintm  13772  subsubrng  14215  subsubrg  14246  lssintclm  14385  lspss  14400  lspun  14403  lsslsp  14430  ntrss  14830  neiint  14856  neiss  14861  restopnb  14892  iscnp4  14929  blssps  15138  blss  15139  xmettx  15221  tgqioo  15266  rescncf  15292  suplociccreex  15335  suplociccex  15336  dvbss  15396  dvbsssg  15397  dvfgg  15399  dvidsslem  15404  dvconstss  15409  dvcnp2cntop  15410  dvcn  15411  dvaddxxbr  15412  dvmulxxbr  15413  dvcoapbr  15418