Metamath Proof Explorer

Theorem psssstr

Description: Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996)

Ref Expression
Assertion psssstr ⊢ A ⊂ B ∧ B ⊆ C → A ⊂ C

Proof

Step Hyp Ref Expression
1 sspss ⊢ B ⊆ C ↔ B ⊂ C ∨ B = C
2 psstr ⊢ A ⊂ B ∧ B ⊂ C → A ⊂ C
3 2 ex ⊢ A ⊂ B → B ⊂ C → A ⊂ C
4 psseq2 ⊢ B = C → A ⊂ B ↔ A ⊂ C
5 4 biimpcd ⊢ A ⊂ B → B = C → A ⊂ C
6 3 5 jaod ⊢ A ⊂ B → B ⊂ C ∨ B = C → A ⊂ C
7 6 imp ⊢ A ⊂ B ∧ B ⊂ C ∨ B = C → A ⊂ C
8 1 7 sylan2b ⊢ A ⊂ B ∧ B ⊆ C → A ⊂ C