Metamath Proof Explorer

Theorem bj-19.23t

Description: Statement 19.23t proved from modalK (obsoleting 19.23v ). (Contributed by BJ, 2-Dec-2023)

Ref Expression
Assertion bj-19.23t ⊢ Ⅎ' x ψ → ∀ x φ → ψ ↔ ∃ x φ → ψ

Proof

Step Hyp Ref Expression
1 bj-nnf-exlim ⊢ Ⅎ' x ψ → ∀ x φ → ψ → ∃ x φ → ψ
2 bj-nnfa ⊢ Ⅎ' x ψ → ψ → ∀ x ψ
3 2 imim2d ⊢ Ⅎ' x ψ → ∃ x φ → ψ → ∃ x φ → ∀ x ψ
4 19.38 ⊢ ∃ x φ → ∀ x ψ → ∀ x φ → ψ
5 3 4 syl6 ⊢ Ⅎ' x ψ → ∃ x φ → ψ → ∀ x φ → ψ
6 1 5 impbid ⊢ Ⅎ' x ψ → ∀ x φ → ψ ↔ ∃ x φ → ψ