This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sseqtrrdi

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

Ref Expression
Hypotheses sseqtrrdi.1 ⊢ φ → A ⊆ B
sseqtrrdi.2 ⊢ C = B
Assertion sseqtrrdi ⊢ φ → A ⊆ C

Proof

Step Hyp Ref Expression
1 sseqtrrdi.1 ⊢ φ → A ⊆ B
2 sseqtrrdi.2 ⊢ C = B
3 2 eqcomi ⊢ B = C
4 1 3 sseqtrdi ⊢ φ → A ⊆ C