Metamath Proof Explorer

Theorem ordtr1

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

Ref Expression
Assertion ordtr1 
|- ( Ord C -> ( ( A e. B /\ B e. C ) -> A e. C ) )

Proof

Step Hyp Ref Expression
1 ordtr 
 |-  ( Ord C -> Tr C )
2 trel 
 |-  ( Tr C -> ( ( A e. B /\ B e. C ) -> A e. C ) )
3 1 2 syl 
 |-  ( Ord C -> ( ( A e. B /\ B e. C ) -> A e. C ) )