Theorem sstrdi 3179

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

Syntax hints:   → wi 4   ⊆ wss 3141

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154

This theorem is referenced by:  difss2  3275  sstpr  3769  rintm  3991  eqbrrdva  4809  dmxpss2  5073  rnxpss2  5074  ssxpbm  5076  ssxp1  5077  ssxp2  5078  relfld  5169  funssxp  5397  dff2  5673  fliftf  5813  1stcof  6178  2ndcof  6179  tfrlemibfn  6343  tfr1onlembfn  6359  tfrcllemssrecs  6367  tfrcllembfn  6372  sucinc2  6461  peano5nnnn  7905  peano5nni  8936  suprzclex  9365  ioodisj  10007  fzssnn  10082  fzossnn0  10189  elfzom1elp1fzo  10216  frecuzrdgtcl  10426  frecuzrdgdomlem  10431  frecuzrdgfunlem  10433  zfz1iso  10835  seq3coll  10836  summodclem2a  11403  summodclem2  11404  zsumdc  11406  fsumsersdc  11417  fsum3cvg3  11418  prodmodclem2a  11598  prodmodclem2  11599  zproddc  11601  exmidunben  12441  nninfdclemp1  12465  strsetsid  12509  reldvdsrsrg  13340  lmss  14042  dvbssntrcntop  14449  dvcjbr  14468  reeff1olem  14488  peano5set  14988