Theorem chneq12

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

	Ref	Expression
Assertion	chneq12	⊢ ( ( < = 𝑅 ∧ 𝐴 = 𝐵 ) → ( < Chain 𝐴 ) = ( 𝑅 Chain 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		chneq1	⊢ ( < = 𝑅 → ( < Chain 𝐴 ) = ( 𝑅 Chain 𝐴 ) )
2		chneq2	⊢ ( 𝐴 = 𝐵 → ( 𝑅 Chain 𝐴 ) = ( 𝑅 Chain 𝐵 ) )
3	1 2	sylan9eq	⊢ ( ( < = 𝑅 ∧ 𝐴 = 𝐵 ) → ( < Chain 𝐴 ) = ( 𝑅 Chain 𝐵 ) )