Metamath Proof Explorer

Theorem bj-wnf1

Description: When ph is substituted for ps , this is the first half of nonfreness ( . -> A. ) of the weak form of nonfreeness ( E. -> A. ) . (Contributed by BJ, 9-Dec-2023)

Ref Expression
Assertion bj-wnf1 ⊢ ∃ x φ → ∀ x ψ → ∀ x ∃ x φ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 bj-modal4e ⊢ ∃ x ∃ x φ → ∃ x φ
2 hba1 ⊢ ∀ x ψ → ∀ x ∀ x ψ
3 1 2 imim12i ⊢ ∃ x φ → ∀ x ψ → ∃ x ∃ x φ → ∀ x ∀ x ψ
4 19.38 ⊢ ∃ x ∃ x φ → ∀ x ∀ x ψ → ∀ x ∃ x φ → ∀ x ψ
5 3 4 syl ⊢ ∃ x φ → ∀ x ψ → ∀ x ∃ x φ → ∀ x ψ