Metamath Proof Explorer

Theorem bj-nfimt

Description: Closed form of nfim and curried (exported) form of nfimt . (Contributed by BJ, 20-Oct-2021)

Ref Expression
Assertion bj-nfimt ⊢ Ⅎ x φ → Ⅎ x ψ → Ⅎ x φ → ψ

Proof

Step Hyp Ref Expression
1 19.35 ⊢ ∃ x φ → ψ ↔ ∀ x φ → ∃ x ψ
2 id ⊢ Ⅎ x φ → Ⅎ x φ
3 2 nfrd ⊢ Ⅎ x φ → ∃ x φ → ∀ x φ
4 3 imim1d ⊢ Ⅎ x φ → ∀ x φ → ∃ x ψ → ∃ x φ → ∃ x ψ
5 1 4 syl5bi ⊢ Ⅎ x φ → ∃ x φ → ψ → ∃ x φ → ∃ x ψ
6 id ⊢ Ⅎ x ψ → Ⅎ x ψ
7 6 nfrd ⊢ Ⅎ x ψ → ∃ x ψ → ∀ x ψ
8 7 imim2d ⊢ Ⅎ x ψ → ∃ x φ → ∃ x ψ → ∃ x φ → ∀ x ψ
9 19.38 ⊢ ∃ x φ → ∀ x ψ → ∀ x φ → ψ
10 8 9 syl6 ⊢ Ⅎ x ψ → ∃ x φ → ∃ x ψ → ∀ x φ → ψ
11 5 10 syl9 ⊢ Ⅎ x φ → Ⅎ x ψ → ∃ x φ → ψ → ∀ x φ → ψ
12 df-nf ⊢ Ⅎ x φ → ψ ↔ ∃ x φ → ψ → ∀ x φ → ψ
13 11 12 syl6ibr ⊢ Ⅎ x φ → Ⅎ x ψ → Ⅎ x φ → ψ