**Description:** Closed form of nfnth . (Contributed by BJ, 16-Sep-2021) (Proof
shortened by Wolf Lammen, 4-Sep-2022)

Ref | Expression | ||
---|---|---|---|

Assertion | nfntht | $${\u22a2}\neg \exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \u2132{x}\phantom{\rule{.4em}{0ex}}{\phi}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | pm2.21 | $${\u22a2}\neg \exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi}\right)$$ | |

2 | 1 | nfd | $${\u22a2}\neg \exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \u2132{x}\phantom{\rule{.4em}{0ex}}{\phi}$$ |