Theorem sseqtrrdi 3275

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

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

Assertion

Ref	Expression
sseqtrrdi	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrrdi

Step	Hyp	Ref	Expression
1		sseqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2234	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtrdi 3274	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1397   ⊆ wss 3199

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212

This theorem is referenced by:  iunpw  4579  iotanul  5304  iotass  5306  tfrlem9  6490  tfrlemibfn  6499  tfrlemiubacc  6501  tfrlemi14d  6504  tfr1onlemssrecs  6510  tfr1onlemres  6520  tfrcllemres  6533  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  uznnssnn  9816  pfxccatpfx2  11327  shftfvalg  11401  shftfval  11404  clim2prod  12123  dvdsrvald  14131  dvdsrex  14136  eltopss  14762  difopn  14861  tgrest  14922  txuni2  15009  tgioo  15307  plycoeid3  15510