Description: If in a context x is not free in ps and ch , then it is not free in ( ps -> ch ) . Deduction form of nfim . (Contributed by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 30-Dec-2017) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021) Eliminate curried form of nfimt . (Revised by Wolf Lammen, 10-Jul-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfimd.1 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) | |
| nfimd.2 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) | ||
| Assertion | nfimd | ⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 → 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfimd.1 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) | |
| 2 | nfimd.2 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) | |
| 3 | 19.35 | ⊢ ( ∃ 𝑥 ( 𝜓 → 𝜒 ) ↔ ( ∀ 𝑥 𝜓 → ∃ 𝑥 𝜒 ) ) | |
| 4 | 3 | biimpi | ⊢ ( ∃ 𝑥 ( 𝜓 → 𝜒 ) → ( ∀ 𝑥 𝜓 → ∃ 𝑥 𝜒 ) ) |
| 5 | 1 | nfrd | ⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) ) |
| 6 | 2 | nfrd | ⊢ ( 𝜑 → ( ∃ 𝑥 𝜒 → ∀ 𝑥 𝜒 ) ) |
| 7 | 5 6 | imim12d | ⊢ ( 𝜑 → ( ( ∀ 𝑥 𝜓 → ∃ 𝑥 𝜒 ) → ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) ) |
| 8 | 19.38 | ⊢ ( ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) → ∀ 𝑥 ( 𝜓 → 𝜒 ) ) | |
| 9 | 4 7 8 | syl56 | ⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝜓 → 𝜒 ) → ∀ 𝑥 ( 𝜓 → 𝜒 ) ) ) |
| 10 | 9 | nfd | ⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 → 𝜒 ) ) |