Theorem sstrd 3165

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

Syntax hints:   → wi 4   ⊆ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  sstrid  3166  sstrdi  3167  ssdif2d  3274  tfisi  4586  funss  5235  fssxp  5383  fvmptssdm  5600  suppssfv  6078  suppssov1  6079  tposss  6246  tfrlem1  6308  tfrlemibfn  6328  tfr1onlembfn  6344  tfr1onlemubacc  6346  tfr1onlemres  6349  tfrcllembfn  6357  tfrcllemubacc  6359  tfrcllemres  6362  ecinxp  6609  undifdc  6922  sbthlem1  6955  iseqf1olemnab  10485  fiubm  10803  isumss  11394  prodssdc  11592  ennnfoneleminc  12406  strsetsid  12489  strleund  12556  strext  12558  imasaddvallemg  12718  subsubg  13010  subgintm  13011  subsubrg  13326  ntrss  13512  neiint  13538  neiss  13543  restopnb  13574  iscnp4  13611  blssps  13820  blss  13821  xmettx  13903  tgqioo  13940  rescncf  13961  suplociccreex  13995  suplociccex  13996  dvbss  14047  dvbsssg  14048  dvfgg  14050  dvcnp2cntop  14056  dvcn  14057  dvaddxxbr  14058  dvmulxxbr  14059  dvcoapbr  14064