Metamath Proof Explorer

Theorem ordtr1

Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004)

Ref Expression
Assertion ordtr1 ⊢ Ord ⁡ C → A ∈ B ∧ B ∈ C → A ∈ C

Proof

Step Hyp Ref Expression
1 ordtr ⊢ Ord ⁡ C → Tr ⁡ C
2 trel ⊢ Tr ⁡ C → A ∈ B ∧ B ∈ C → A ∈ C
3 1 2 syl ⊢ Ord ⁡ C → A ∈ B ∧ B ∈ C → A ∈ C