Theorem sstrdi 3260

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 3258	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  difss2  3357  sstpr  3880  rintm  4103  eqbrrdva  4948  dmxpss2  5218  rnxpss2  5219  ssxpbm  5221  ssxp1  5222  ssxp2  5223  relfld  5314  funssxp  5555  dff2  5846  fliftf  5999  1stcof  6391  2ndcof  6392  tfrlemibfn  6593  tfr1onlembfn  6609  tfrcllemssrecs  6617  tfrcllembfn  6622  sucinc2  6713  peano5nnnn  8253  peano5nni  9290  suprzclex  9727  ioodisj  10378  fzssnn  10457  fzossnn0  10567  elfzom1elp1fzo  10603  frecuzrdgtcl  10832  frecuzrdgdomlem  10837  frecuzrdgfunlem  10839  zfz1iso  11276  seq3coll  11277  summodclem2a  12131  summodclem2  12132  zsumdc  12134  fsumsersdc  12145  fsum3cvg3  12146  prodmodclem2a  12326  prodmodclem2  12327  zproddc  12329  4sqlem11  13163  ballotfilemfc0  13215  ballotfilemsima  13242  exmidunben  13300  nninfdclemp1  13324  strsetsid  13368  lmss  15330  dvbssntrcntop  15768  dvcjbr  15792  reeff1olem  15855  peano5set  16949