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  3835  rintm  4058  eqbrrdva  4892  dmxpss2  5161  rnxpss2  5162  ssxpbm  5164  ssxp1  5165  ssxp2  5166  relfld  5257  funssxp  5495  dff2  5781  fliftf  5929  1stcof  6315  2ndcof  6316  tfrlemibfn  6480  tfr1onlembfn  6496  tfrcllemssrecs  6504  tfrcllembfn  6509  sucinc2  6600  peano5nnnn  8090  peano5nni  9124  suprzclex  9556  ioodisj  10201  fzssnn  10276  fzossnn0  10385  elfzom1elp1fzo  10420  frecuzrdgtcl  10646  frecuzrdgdomlem  10651  frecuzrdgfunlem  10653  zfz1iso  11076  seq3coll  11077  summodclem2a  11907  summodclem2  11908  zsumdc  11910  fsumsersdc  11921  fsum3cvg3  11922  prodmodclem2a  12102  prodmodclem2  12103  zproddc  12105  4sqlem11  12939  exmidunben  13012  nninfdclemp1  13036  strsetsid  13080  lmss  14935  dvbssntrcntop  15373  dvcjbr  15397  reeff1olem  15460  peano5set  16358