Metamath Proof Explorer


Theorem nfntht2

Description: Closed form of nfnth . (Contributed by BJ, 16-Sep-2021) (Proof shortened by Wolf Lammen, 4-Sep-2022)

Ref Expression
Assertion nfntht2 ( ∀ 𝑥 ¬ 𝜑 → Ⅎ 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 alnex ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
2 nfntht ( ¬ ∃ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 )
3 1 2 sylbi ( ∀ 𝑥 ¬ 𝜑 → Ⅎ 𝑥 𝜑 )