Theorem ontr1i

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

	Ref	Expression
Hypotheses	ontr1i.1	$$⊢C\in \mathrm{On}$$
	ontr1i.2	$$⊢A\in B$$
	ontr1i.3	$$⊢B\in C$$
Assertion	ontr1i	$$⊢A\in C$$

Proof

Step	Hyp	Ref	Expression
1		ontr1i.1	$$⊢C\in \mathrm{On}$$
2		ontr1i.2	$$⊢A\in B$$
3		ontr1i.3	$$⊢B\in C$$
4		ontr1	$$⊢C\in \mathrm{On}\to \left(\left(A\in B\wedge B\in C\right)\to A\in C\right)$$
5	2 3 4	mp2ani	$$⊢C\in \mathrm{On}\to A\in C$$
6	1 5	ax-mp	$$⊢A\in C$$