Metamath Proof Explorer


Theorem ontr2

Description: Transitive law for ordinal numbers. Exercise 3 of TakeutiZaring p. 40. (Contributed by NM, 6-Nov-2003)

Ref Expression
Assertion ontr2 A On C On A B B C A C

Proof

Step Hyp Ref Expression
1 eloni A On Ord A
2 eloni C On Ord C
3 ordtr2 Ord A Ord C A B B C A C
4 1 2 3 syl2an A On C On A B B C A C