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 1847. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
nfnd.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nfnd | ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfnd.1 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
2 | nfnt 1847 | . 2 ⊢ (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-or 842 df-ex 1772 df-nf 1776 |
This theorem is referenced by: nfand 1889 nfan1 2190 hbnt 2293 nfexd 2339 cbvexdw 2350 cbvexd 2420 nfexd2 2460 nfned 3117 nfneld 3128 nfrexd 3304 nfrexdg 3305 vtoclgft 3551 axpowndlem3 10009 axpowndlem4 10010 axregndlem2 10013 axregnd 10014 distel 32945 bj-cbvexdv 34019 bj-nfexd 34322 |
Copyright terms: Public domain | W3C validator |