Theorem ontr1i

Description: Transitive law for ordinal numbers. Inference form of ontr1 . (Contributed by BTernaryTau, 19-Oct-2026)

	Ref	Expression
Hypotheses	ontr1i.1	|- C e. On
	ontr1i.2	|- A e. B
	ontr1i.3	|- B e. C
Assertion	ontr1i	|- A e. C

Proof

Step	Hyp	Ref	Expression
1		ontr1i.1	|- C e. On
2		ontr1i.2	|- A e. B
3		ontr1i.3	|- B e. C
4		ontr1	|- ( C e. On -> ( ( A e. B /\ B e. C ) -> A e. C ) )
5	2 3 4	mp2ani	|- ( C e. On -> A e. C )
6	1 5	ax-mp	|- A e. C