Metamath Proof Explorer


Theorem equsexvw

Description: Version of equsexv with a disjoint variable condition, and of equsex with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw . (Contributed by BJ, 31-May-2019) (Proof shortened by Wolf Lammen, 23-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 equsalvw.1 x = y φ ψ
2 alinexa x x = y ¬ φ ¬ x x = y φ
3 1 notbid x = y ¬ φ ¬ ψ
4 3 equsalvw x x = y ¬ φ ¬ ψ
5 2 4 bitr3i ¬ x x = y φ ¬ ψ
6 5 con4bii x x = y φ ψ