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 ) ) |
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 ) ) |