Metamath Proof Explorer


Theorem 19.9dev

Description: 19.9d in the case of an existential quantifier, avoiding the ax-10 from nfex that would be used for the hypothesis of 19.9d , at the cost of an additional DV condition on y , ph . (Contributed by SN, 26-May-2024)

Ref Expression
Hypothesis 19.9dev.1 φ x ψ
Assertion 19.9dev φ x y ψ y ψ

Proof

Step Hyp Ref Expression
1 19.9dev.1 φ x ψ
2 excom x y ψ y x ψ
3 19.9t x ψ x ψ ψ
4 1 3 syl φ x ψ ψ
5 4 exbidv φ y x ψ y ψ
6 2 5 syl5bb φ x y ψ y ψ