Metamath Proof Explorer


Theorem nftht

Description: Closed form of nfth . (Contributed by Wolf Lammen, 19-Aug-2018) (Proof shortened by BJ, 16-Sep-2021) (Proof shortened by Wolf Lammen, 3-Sep-2022)

Ref Expression
Assertion nftht ( ∀ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 ax-1 ( ∀ 𝑥 𝜑 → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) )
2 1 nfd ( ∀ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 )