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

Proof

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