Metamath Proof Explorer

Theorem bj-nfimt

Description: Closed form of nfim and curried (exported) form of nfimt . (Contributed by BJ, 20-Oct-2021) Proof should not use 19.35 . (Proof modification is discouraged.)

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

Proof

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