| 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 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-or 849 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: nfand 1897 nfan1 2200 hbnt 2294 nfexd 2329 cbvexdw 2341 cbvexd 2413 nfexd2 2451 nfned 3044 nfneld 3055 nfrexdw 3310 nfrexd 3373 cbvexeqsetf 3495 axpowndlem3 10639 axpowndlem4 10640 axregndlem2 10643 axregnd 10644 cbvex1v 35088 axnulg 35106 distel 35804 bj-cbvexdv 36801 bj-nfexd 37139 wl-issetft 37583 |
| Copyright terms: Public domain | W3C validator |