Theorem sstrid 3259

Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)

Hypotheses

Ref	Expression
sstrid.1	⊢ 𝐴 ⊆ 𝐵
sstrid.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
sstrid	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrid

Step	Hyp	Ref	Expression
1		sstrid.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3		sstrid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	sstrd 3258	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  cossxp2  5311  fimass  5550  fimacnv  5837  smores2  6565  f1imaen2g  7080  phplem4dom  7163  isinfinf  7201  fidcenumlemrk  7271  casef  7429  genipv  7877  fzossnn0  10595  seq3split  10940  1arith  13169  ballotfilemsima  13311  ctinf  13373  nninfdclemcl  13391  nninfdclemp1  13393  mhmima  13851  cntzmhm  14167  znleval  15072  tgcl  15256  epttop  15282  ntrin  15316  cnconst2  15425  cnrest2  15428  cnptopresti  15430  cnptoprest2  15432  hmeores  15507  blin2  15624  ivthdec  15836  limcdifap  15854  limcresi  15858  dvfgg  15880  dvcnp2cntop  15891  dvaddxxbr  15893  reeff1olem  15963  ppiqsval  16201  prmdvdsfi  16204  domomsubct  17197