Description: A closed form of nfim . (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 2-Jan-2018) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfim1.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| nfim1.2 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) | ||
| Assertion | nfim1 | ⊢ Ⅎ 𝑥 ( 𝜑 → 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfim1.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| 2 | nfim1.2 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) | |
| 3 | nf3 | ⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) ) | |
| 4 | 1 3 | mpbi | ⊢ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) |
| 5 | nftht | ⊢ ( ∀ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 ) | |
| 6 | 2 | sps | ⊢ ( ∀ 𝑥 𝜑 → Ⅎ 𝑥 𝜓 ) |
| 7 | 5 6 | nfimd | ⊢ ( ∀ 𝑥 𝜑 → Ⅎ 𝑥 ( 𝜑 → 𝜓 ) ) |
| 8 | pm2.21 | ⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) ) | |
| 9 | 8 | alimi | ⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) |
| 10 | nftht | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → Ⅎ 𝑥 ( 𝜑 → 𝜓 ) ) | |
| 11 | 9 10 | syl | ⊢ ( ∀ 𝑥 ¬ 𝜑 → Ⅎ 𝑥 ( 𝜑 → 𝜓 ) ) |
| 12 | 7 11 | jaoi | ⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) → Ⅎ 𝑥 ( 𝜑 → 𝜓 ) ) |
| 13 | 4 12 | ax-mp | ⊢ Ⅎ 𝑥 ( 𝜑 → 𝜓 ) |