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
|- ( A. x ph -> F/ x ph )

Proof

Step Hyp Ref Expression
1 ax-1
 |-  ( A. x ph -> ( E. x ph -> A. x ph ) )
2 1 nfd
 |-  ( A. x ph -> F/ x ph )