Theorem chneq12

Description: Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026)

	Ref	Expression
Assertion	chneq12	$$⊢\left(\underset{\dot{}}{<}=R\wedge A=B\right)\to {\mathrm{Chain}}_A\underset{\dot{}}{<}={\mathrm{Chain}}_{B}R$$

Proof

Step	Hyp	Ref	Expression
1		chneq1	$$⊢\underset{\dot{}}{<}=R\to {\mathrm{Chain}}_A\underset{\dot{}}{<}={\mathrm{Chain}}_{A}R$$
2		chneq2	$$⊢A=B\to {\mathrm{Chain}}_{A}R={\mathrm{Chain}}_{B}R$$
3	1 2	sylan9eq	$$⊢\left(\underset{\dot{}}{<}=R\wedge A=B\right)\to {\mathrm{Chain}}_A\underset{\dot{}}{<}={\mathrm{Chain}}_{B}R$$