Theorem sstrdi 3240

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
sstrdi.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sstrdi.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
sstrdi	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrdi

Step	Hyp	Ref	Expression
1		sstrdi.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sstrdi.2	. . 3 ⊢ 𝐵 ⊆ 𝐶
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	1, 3	sstrd 3238	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  difss2  3337  sstpr  3845  rintm  4068  eqbrrdva  4906  dmxpss2  5176  rnxpss2  5177  ssxpbm  5179  ssxp1  5180  ssxp2  5181  relfld  5272  funssxp  5512  dff2  5799  fliftf  5950  1stcof  6335  2ndcof  6336  tfrlemibfn  6537  tfr1onlembfn  6553  tfrcllemssrecs  6561  tfrcllembfn  6566  sucinc2  6657  peano5nnnn  8155  peano5nni  9188  suprzclex  9622  ioodisj  10272  fzssnn  10348  fzossnn0  10457  elfzom1elp1fzo  10493  frecuzrdgtcl  10720  frecuzrdgdomlem  10725  frecuzrdgfunlem  10727  zfz1iso  11151  seq3coll  11152  summodclem2a  12005  summodclem2  12006  zsumdc  12008  fsumsersdc  12019  fsum3cvg3  12020  prodmodclem2a  12200  prodmodclem2  12201  zproddc  12203  4sqlem11  13037  exmidunben  13110  nninfdclemp1  13134  strsetsid  13178  lmss  15040  dvbssntrcntop  15478  dvcjbr  15502  reeff1olem  15565  peano5set  16639