Theorem sstrid 3166

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 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:  cossxp2  5149  fimacnv  5642  smores2  6290  f1imaen2g  6788  phplem4dom  6857  isinfinf  6892  fidcenumlemrk  6948  casef  7082  genipv  7503  fzossnn0  10168  seq3split  10472  1arith  12355  ctinf  12421  nninfdclemcl  12439  nninfdclemp1  12441  mhmima  12803  tgcl  13346  epttop  13372  ntrin  13406  cnconst2  13515  cnrest2  13518  cnptopresti  13520  cnptoprest2  13522  hmeores  13597  blin2  13714  ivthdec  13904  limcdifap  13913  limcresi  13917  dvfgg  13939  dvcnp2cntop  13945  dvaddxxbr  13947  reeff1olem  13974