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	⊢ ( Ⅎ 𝑥 𝜑 → ( Ⅎ 𝑥 𝜓 → Ⅎ 𝑥 ( 𝜑 → 𝜓 ) ) )

Proof

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