Theorem sstrdi 3159

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

Syntax hints:   → wi 4   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  difss2  3255  sstpr  3744  rintm  3965  eqbrrdva  4781  dmxpss2  5043  rnxpss2  5044  ssxpbm  5046  ssxp1  5047  ssxp2  5048  relfld  5139  funssxp  5367  dff2  5640  fliftf  5778  1stcof  6142  2ndcof  6143  tfrlemibfn  6307  tfr1onlembfn  6323  tfrcllemssrecs  6331  tfrcllembfn  6336  sucinc2  6425  peano5nnnn  7854  peano5nni  8881  suprzclex  9310  ioodisj  9950  fzssnn  10024  fzossnn0  10131  elfzom1elp1fzo  10158  frecuzrdgtcl  10368  frecuzrdgdomlem  10373  frecuzrdgfunlem  10375  zfz1iso  10776  seq3coll  10777  summodclem2a  11344  summodclem2  11345  zsumdc  11347  fsumsersdc  11358  fsum3cvg3  11359  prodmodclem2a  11539  prodmodclem2  11540  zproddc  11542  exmidunben  12381  nninfdclemp1  12405  strsetsid  12449  lmss  13040  dvbssntrcntop  13447  dvcjbr  13466  reeff1olem  13486  peano5set  13975