Metamath Proof Explorer


Theorem nfnth

Description: No variable is (effectively) free in a non-theorem. (Contributed by Mario Carneiro, 6-Dec-2016) df-nf changed. (Revised by Wolf Lammen, 12-Sep-2021)

Ref Expression
Hypothesis nfnth.1 ¬ 𝜑
Assertion nfnth 𝑥 𝜑

Proof

Step Hyp Ref Expression
1 nfnth.1 ¬ 𝜑
2 nfntht2 ( ∀ 𝑥 ¬ 𝜑 → Ⅎ 𝑥 𝜑 )
3 2 1 mpg 𝑥 𝜑