Theorem sstrdi 3114

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

Syntax hints:   → wi 4   ⊆ wss 3076

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  difss2  3209  sstpr  3692  rintm  3913  eqbrrdva  4717  dmxpss2  4979  rnxpss2  4980  ssxpbm  4982  ssxp1  4983  ssxp2  4984  relfld  5075  funssxp  5300  dff2  5572  fliftf  5708  1stcof  6069  2ndcof  6070  tfrlemibfn  6233  tfr1onlembfn  6249  tfrcllemssrecs  6257  tfrcllembfn  6262  sucinc2  6350  peano5nnnn  7724  peano5nni  8747  suprzclex  9173  ioodisj  9806  fzssnn  9879  fzossnn0  9983  elfzom1elp1fzo  10010  frecuzrdgtcl  10216  frecuzrdgdomlem  10221  frecuzrdgfunlem  10223  zfz1iso  10616  seq3coll  10617  summodclem2a  11182  summodclem2  11183  zsumdc  11185  fsumsersdc  11196  fsum3cvg3  11197  prodmodclem2a  11377  prodmodclem2  11378  zproddc  11380  exmidunben  11975  strsetsid  12031  lmss  12454  dvbssntrcntop  12861  dvcjbr  12880  reeff1olem  12900  peano5set  13309