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 φ