Theorem sstrdi 3236

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 3234	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:  difss2  3332  sstpr  3834  rintm  4057  eqbrrdva  4891  dmxpss2  5160  rnxpss2  5161  ssxpbm  5163  ssxp1  5164  ssxp2  5165  relfld  5256  funssxp  5492  dff2  5778  fliftf  5922  1stcof  6307  2ndcof  6308  tfrlemibfn  6472  tfr1onlembfn  6488  tfrcllemssrecs  6496  tfrcllembfn  6501  sucinc2  6590  peano5nnnn  8075  peano5nni  9109  suprzclex  9541  ioodisj  10185  fzssnn  10260  fzossnn0  10369  elfzom1elp1fzo  10403  frecuzrdgtcl  10629  frecuzrdgdomlem  10634  frecuzrdgfunlem  10636  zfz1iso  11058  seq3coll  11059  summodclem2a  11887  summodclem2  11888  zsumdc  11890  fsumsersdc  11901  fsum3cvg3  11902  prodmodclem2a  12082  prodmodclem2  12083  zproddc  12085  4sqlem11  12919  exmidunben  12992  nninfdclemp1  13016  strsetsid  13060  reldvdsrsrg  14050  lmss  14914  dvbssntrcntop  15352  dvcjbr  15376  reeff1olem  15439  peano5set  16261