Metamath Proof Explorer
Description: Closed form of nfnth . (Contributed by BJ, 16-Sep-2021) (Proof
shortened by Wolf Lammen, 4-Sep-2022)
|
|
Ref |
Expression |
|
Assertion |
nfntht2 |
⊢ ( ∀ 𝑥 ¬ 𝜑 → Ⅎ 𝑥 𝜑 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
alnex |
⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 ) |
2 |
|
nfntht |
⊢ ( ¬ ∃ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 ) |
3 |
1 2
|
sylbi |
⊢ ( ∀ 𝑥 ¬ 𝜑 → Ⅎ 𝑥 𝜑 ) |