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 ) |
| 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 ) |