Theorem sstrdi 3167

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

Syntax hints:   → wi 4   ⊆ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  difss2  3263  sstpr  3756  rintm  3977  eqbrrdva  4794  dmxpss2  5058  rnxpss2  5059  ssxpbm  5061  ssxp1  5062  ssxp2  5063  relfld  5154  funssxp  5382  dff2  5657  fliftf  5795  1stcof  6159  2ndcof  6160  tfrlemibfn  6324  tfr1onlembfn  6340  tfrcllemssrecs  6348  tfrcllembfn  6353  sucinc2  6442  peano5nnnn  7886  peano5nni  8916  suprzclex  9345  ioodisj  9987  fzssnn  10061  fzossnn0  10168  elfzom1elp1fzo  10195  frecuzrdgtcl  10405  frecuzrdgdomlem  10410  frecuzrdgfunlem  10412  zfz1iso  10812  seq3coll  10813  summodclem2a  11380  summodclem2  11381  zsumdc  11383  fsumsersdc  11394  fsum3cvg3  11395  prodmodclem2a  11575  prodmodclem2  11576  zproddc  11578  exmidunben  12417  nninfdclemp1  12441  strsetsid  12485  reldvdsrsrg  13160  lmss  13528  dvbssntrcntop  13935  dvcjbr  13954  reeff1olem  13974  peano5set  14463