![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfnd | Structured version Visualization version GIF version |
Description: Deduction associated with nfnt 1857. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
nfnd.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nfnd | ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfnd.1 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
2 | nfnt 1857 | . 2 ⊢ (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 210 df-or 845 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nfand 1898 nfan1 2198 hbnt 2298 nfexd 2337 cbvexdw 2348 cbvexd 2418 nfexd2 2457 nfned 3088 nfneld 3099 nfrexd 3266 nfrexdg 3267 vtoclgft 3501 axpowndlem3 10010 axpowndlem4 10011 axregndlem2 10014 axregnd 10015 distel 33161 bj-cbvexdv 34237 bj-nfexd 34553 |
Copyright terms: Public domain | W3C validator |