Theorem sstrid 3168

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

Syntax hints:   → wi 4   ⊆ wss 3131

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 3137  df-ss 3144

This theorem is referenced by:  cossxp2  5154  fimacnv  5648  smores2  6298  f1imaen2g  6796  phplem4dom  6865  isinfinf  6900  fidcenumlemrk  6956  casef  7090  genipv  7511  fzossnn0  10178  seq3split  10482  1arith  12368  ctinf  12434  nninfdclemcl  12452  nninfdclemp1  12454  mhmima  12881  tgcl  13704  epttop  13730  ntrin  13764  cnconst2  13873  cnrest2  13876  cnptopresti  13878  cnptoprest2  13880  hmeores  13955  blin2  14072  ivthdec  14262  limcdifap  14271  limcresi  14275  dvfgg  14297  dvcnp2cntop  14303  dvaddxxbr  14305  reeff1olem  14332