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 1856. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
nfnd.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nfnd | ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfnd.1 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
2 | nfnt 1856 | . 2 ⊢ (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 Ⅎwnf 1784 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 209 df-or 844 df-ex 1781 df-nf 1785 |
This theorem is referenced by: nfand 1898 nfan1 2200 hbnt 2302 nfexd 2348 cbvexdw 2359 cbvexd 2429 nfexd2 2468 nfned 3122 nfneld 3133 nfrexd 3309 nfrexdg 3310 vtoclgft 3555 axpowndlem3 10023 axpowndlem4 10024 axregndlem2 10027 axregnd 10028 distel 33050 bj-cbvexdv 34124 bj-nfexd 34432 |
Copyright terms: Public domain | W3C validator |