Theorem sstrdi 3191

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

Syntax hints:   → wi 4   ⊆ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  difss2  3287  sstpr  3783  rintm  4005  eqbrrdva  4832  dmxpss2  5098  rnxpss2  5099  ssxpbm  5101  ssxp1  5102  ssxp2  5103  relfld  5194  funssxp  5423  dff2  5702  fliftf  5842  1stcof  6216  2ndcof  6217  tfrlemibfn  6381  tfr1onlembfn  6397  tfrcllemssrecs  6405  tfrcllembfn  6410  sucinc2  6499  peano5nnnn  7952  peano5nni  8985  suprzclex  9415  ioodisj  10059  fzssnn  10134  fzossnn0  10242  elfzom1elp1fzo  10269  frecuzrdgtcl  10483  frecuzrdgdomlem  10488  frecuzrdgfunlem  10490  zfz1iso  10912  seq3coll  10913  summodclem2a  11524  summodclem2  11525  zsumdc  11527  fsumsersdc  11538  fsum3cvg3  11539  prodmodclem2a  11719  prodmodclem2  11720  zproddc  11722  4sqlem11  12539  exmidunben  12583  nninfdclemp1  12607  strsetsid  12651  reldvdsrsrg  13588  lmss  14414  dvbssntrcntop  14838  dvcjbr  14857  reeff1olem  14906  peano5set  15432