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

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

Proof

Step Hyp Ref Expression
1 19.35 ⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
2 id ⊢ ( Ⅎ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 )
3 2 nfrd ⊢ ( Ⅎ 𝑥 𝜑 → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) )
4 3 imim1d ⊢ ( Ⅎ 𝑥 𝜑 → ( ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) )
5 1 4 biimtrid ⊢ ( Ⅎ 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) )
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 imbitrrdi ⊢ ( Ⅎ 𝑥 𝜑 → ( Ⅎ 𝑥 𝜓 → Ⅎ 𝑥 ( 𝜑 → 𝜓 ) ) )