Metamath Proof Explorer

Theorem chneq12

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

Ref Expression
Assertion chneq12 
|- ( ( .< = R /\ A = B ) -> ( .< Chain A ) = ( R Chain B ) )

Proof

Step Hyp Ref Expression
1 chneq1 
 |-  ( .< = R -> ( .< Chain A ) = ( R Chain A ) )
2 chneq2 
 |-  ( A = B -> ( R Chain A ) = ( R Chain B ) )
3 1 2 sylan9eq 
 |-  ( ( .< = R /\ A = B ) -> ( .< Chain A ) = ( R Chain B ) )