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

Metamath Proof Explorer

Theorem sseqtrri

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995)

Ref Expression
Hypotheses sseqtrri.1 ⊢ A ⊆ B
sseqtrri.2 ⊢ C = B
Assertion sseqtrri ⊢ A ⊆ C

Proof

Step Hyp Ref Expression
1 sseqtrri.1 ⊢ A ⊆ B
2 sseqtrri.2 ⊢ C = B
3 2 eqcomi ⊢ B = C
4 1 3 sseqtri ⊢ A ⊆ C