Theorem sseqtrrdi 3246

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

Hypotheses

Ref	Expression
sseqtrrdi.1	|- ( ph -> A C_ B )
sseqtrrdi.2	|- C = B

Assertion

Ref	Expression
sseqtrrdi	|- ( ph -> A C_ C )

Proof of Theorem sseqtrrdi

Step	Hyp	Ref	Expression
1		sseqtrrdi.1	. 2 |- ( ph -> A C_ B )
2		sseqtrrdi.2	. . 3 |- C = B
3	2	eqcomi 2210	. 2 |- B = C
4	1, 3	sseqtrdi 3245	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1373   C_ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  iunpw  4540  iotanul  5261  iotass  5263  tfrlem9  6423  tfrlemibfn  6432  tfrlemiubacc  6434  tfrlemi14d  6437  tfr1onlemssrecs  6443  tfr1onlemres  6453  tfrcllemres  6466  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  uznnssnn  9728  shftfvalg  11214  shftfval  11217  clim2prod  11935  reldvdsrsrg  13939  dvdsrvald  13940  dvdsrex  13945  eltopss  14566  difopn  14665  tgrest  14726  txuni2  14813  tgioo  15111  plycoeid3  15314