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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 | |
|
2 | 1 | nfd | |