Metamath Proof Explorer

Theorem ontr1

Description: Transitive law for ordinal numbers. Theorem 7M(b) of Enderton p. 192. (Contributed by NM, 11-Aug-1994)

Ref Expression
Assertion ontr1 
|- ( C e. On -> ( ( A e. B /\ B e. C ) -> A e. C ) )

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( C e. On -> Ord C )
2 ordtr1 
 |-  ( Ord C -> ( ( A e. B /\ B e. C ) -> A e. C ) )
3 1 2 syl 
 |-  ( C e. On -> ( ( A e. B /\ B e. C ) -> A e. C ) )