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

Metamath Proof Explorer

Theorem eqsstrrdi

Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 eqsstrrdi.1 ⊢ φ → B = A
2 eqsstrrdi.2 ⊢ B ⊆ C
3 1 eqcomd ⊢ φ → A = B
4 3 2 eqsstrdi ⊢ φ → A ⊆ C