Description: No variable is (effectively) free in a theorem. (Contributed by Mario Carneiro, 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen, 12-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nfth.1 | ⊢ 𝜑 | |
| Assertion | nfth | ⊢ Ⅎ 𝑥 𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfth.1 | ⊢ 𝜑 | |
| 2 | nftht | ⊢ ( ∀ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 ) | |
| 3 | 2 1 | mpg | ⊢ Ⅎ 𝑥 𝜑 |