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  3882  rintm  4105  eqbrrdva  4950  dmxpss2  5220  rnxpss2  5221  ssxpbm  5223  ssxp1  5224  ssxp2  5225  relfld  5316  funssxp  5557  dff2  5852  fliftf  6005  1stcof  6397  2ndcof  6398  tfrlemibfn  6599  tfr1onlembfn  6615  tfrcllemssrecs  6623  tfrcllembfn  6628  sucinc2  6719  peano5nnnn  8260  peano5nni  9310  suprzclex  9749  ioodisj  10406  fzssnn  10485  fzossnn0  10595  elfzom1elp1fzo  10631  frecuzrdgtcl  10864  frecuzrdgdomlem  10869  frecuzrdgfunlem  10871  zfz1iso  11309  seq3coll  11310  summodclem2a  12167  summodclem2  12168  zsumdc  12170  fsumsersdc  12181  fsum3cvg3  12182  prodmodclem2a  12362  prodmodclem2  12363  zproddc  12365  4sqlem11  13203  ballotfilemfc0  13284  ballotfilemsima  13311  exmidunben  13369  nninfdclemp1  13393  strsetsid  13437  cntzidss  14166  cntzmhm2  14168  lmss  15438  dvbssntrcntop  15876  dvcjbr  15900  reeff1olem  15963  peano5set  17132