Metamath Proof Explorer


Theorem bj-wnfenf

Description: When ph is substituted for ps , this statement expresses that weak nonfreeness implies the existential form of nonfreeness. (Contributed by BJ, 9-Dec-2023)

Ref Expression
Assertion bj-wnfenf x φ x ψ x x φ ψ

Proof

Step Hyp Ref Expression
1 bj-wnf1 x φ x ψ x x φ x ψ
2 bj-19.21bit x φ x ψ x φ ψ
3 1 2 sylg x φ x ψ x x φ ψ