Theorem sstrdi 3204

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

Syntax hints:   → wi 4   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  difss2  3300  sstpr  3797  rintm  4019  eqbrrdva  4846  dmxpss2  5112  rnxpss2  5113  ssxpbm  5115  ssxp1  5116  ssxp2  5117  relfld  5208  funssxp  5439  dff2  5718  fliftf  5858  1stcof  6239  2ndcof  6240  tfrlemibfn  6404  tfr1onlembfn  6420  tfrcllemssrecs  6428  tfrcllembfn  6433  sucinc2  6522  peano5nnnn  7987  peano5nni  9021  suprzclex  9453  ioodisj  10097  fzssnn  10172  fzossnn0  10280  elfzom1elp1fzo  10312  frecuzrdgtcl  10538  frecuzrdgdomlem  10543  frecuzrdgfunlem  10545  zfz1iso  10967  seq3coll  10968  summodclem2a  11611  summodclem2  11612  zsumdc  11614  fsumsersdc  11625  fsum3cvg3  11626  prodmodclem2a  11806  prodmodclem2  11807  zproddc  11809  4sqlem11  12643  exmidunben  12716  nninfdclemp1  12740  strsetsid  12784  reldvdsrsrg  13772  lmss  14636  dvbssntrcntop  15074  dvcjbr  15098  reeff1olem  15161  peano5set  15740