Metamath Proof Explorer


Theorem soeq12d

Description: Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015) (Proof shortened by Matthew House, 10-Sep-2025)

Ref Expression
Hypotheses soeq12d.1
|- ( ph -> R = S )
soeq12d.2
|- ( ph -> A = B )
Assertion soeq12d
|- ( ph -> ( R Or A <-> S Or B ) )

Proof

Step Hyp Ref Expression
1 soeq12d.1
 |-  ( ph -> R = S )
2 soeq12d.2
 |-  ( ph -> A = B )
3 soeq1
 |-  ( R = S -> ( R Or A <-> S Or A ) )
4 soeq2
 |-  ( A = B -> ( S Or A <-> S Or B ) )
5 3 4 sylan9bb
 |-  ( ( R = S /\ A = B ) -> ( R Or A <-> S Or B ) )
6 1 2 5 syl2anc
 |-  ( ph -> ( R Or A <-> S Or B ) )