This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-nnf-exlim

Description: Proof of the closed form of exlimi from modalK (compare exlimiv ). See also bj-sylget2 . (Contributed by BJ, 2-Dec-2023)

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

Proof

Step Hyp Ref Expression
1 exim ⊢ ∀ x φ → ψ → ∃ x φ → ∃ x ψ
2 bj-nnfe ⊢ Ⅎ' x ψ → ∃ x ψ → ψ
3 1 2 syl9r ⊢ Ⅎ' x ψ → ∀ x φ → ψ → ∃ x φ → ψ