Theorem sstrdi 3237

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 3235	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:  difss2  3333  sstpr  3838  rintm  4061  eqbrrdva  4898  dmxpss2  5167  rnxpss2  5168  ssxpbm  5170  ssxp1  5171  ssxp2  5172  relfld  5263  funssxp  5501  dff2  5787  fliftf  5935  1stcof  6321  2ndcof  6322  tfrlemibfn  6489  tfr1onlembfn  6505  tfrcllemssrecs  6513  tfrcllembfn  6518  sucinc2  6609  peano5nnnn  8102  peano5nni  9136  suprzclex  9568  ioodisj  10218  fzssnn  10293  fzossnn0  10402  elfzom1elp1fzo  10437  frecuzrdgtcl  10664  frecuzrdgdomlem  10669  frecuzrdgfunlem  10671  zfz1iso  11095  seq3coll  11096  summodclem2a  11932  summodclem2  11933  zsumdc  11935  fsumsersdc  11946  fsum3cvg3  11947  prodmodclem2a  12127  prodmodclem2  12128  zproddc  12130  4sqlem11  12964  exmidunben  13037  nninfdclemp1  13061  strsetsid  13105  lmss  14960  dvbssntrcntop  15398  dvcjbr  15422  reeff1olem  15485  peano5set  16471