Metamath Proof Explorer

Theorem bj-wnfnf

Description: When ph is substituted for ps , this statement expresses nonfreeness in the weak form of nonfreeness ( E. -> A. ) . Note that this could also be proved from bj-nnfim , bj-nnfe1 and bj-nnfa1 . (Contributed by BJ, 9-Dec-2023)

Ref Expression
Assertion bj-wnfnf ⊢ Ⅎ' x ∃ x φ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 bj-wnf2 ⊢ ∃ x ∃ x φ → ∀ x ψ → ∃ x φ → ∀ x ψ
2 bj-wnf1 ⊢ ∃ x φ → ∀ x ψ → ∀ x ∃ x φ → ∀ x ψ
3 df-bj-nnf ⊢ Ⅎ' x ∃ x φ → ∀ x ψ ↔ ∃ x ∃ x φ → ∀ x ψ → ∃ x φ → ∀ x ψ ∧ ∃ x φ → ∀ x ψ → ∀ x ∃ x φ → ∀ x ψ
4 1 2 3 mpbir2an ⊢ Ⅎ' x ∃ x φ → ∀ x ψ