Metamath Proof Explorer


Theorem weeq12d

Description: Equality deduction for well-orders. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses weeq12d.l ( 𝜑𝑅 = 𝑆 )
weeq12d.r ( 𝜑𝐴 = 𝐵 )
Assertion weeq12d ( 𝜑 → ( 𝑅 We 𝐴𝑆 We 𝐵 ) )

Proof

Step Hyp Ref Expression
1 weeq12d.l ( 𝜑𝑅 = 𝑆 )
2 weeq12d.r ( 𝜑𝐴 = 𝐵 )
3 weeq1 ( 𝑅 = 𝑆 → ( 𝑅 We 𝐴𝑆 We 𝐴 ) )
4 1 3 syl ( 𝜑 → ( 𝑅 We 𝐴𝑆 We 𝐴 ) )
5 weeq2 ( 𝐴 = 𝐵 → ( 𝑆 We 𝐴𝑆 We 𝐵 ) )
6 2 5 syl ( 𝜑 → ( 𝑆 We 𝐴𝑆 We 𝐵 ) )
7 4 6 bitrd ( 𝜑 → ( 𝑅 We 𝐴𝑆 We 𝐵 ) )