Metamath Proof Explorer


Theorem equsalvw

Description: Version of equsalv with a disjoint variable condition, and of equsal with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw . (Contributed by BJ, 31-May-2019)

Ref Expression
Hypothesis equsalvw.1 x = y φ ψ
Assertion equsalvw x x = y φ ψ

Proof

Step Hyp Ref Expression
1 equsalvw.1 x = y φ ψ
2 1 pm5.74i x = y φ x = y ψ
3 2 albii x x = y φ x x = y ψ
4 equsv x x = y ψ ψ
5 3 4 bitri x x = y φ ψ