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 xφxφ

Proof

Step Hyp Ref Expression
1 ax-1 xφxφxφ
2 1 nfd xφxφ