![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nexdv | Structured version Visualization version GIF version |
Description: Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 13-Jul-2020.) (Proof shortened by Wolf Lammen, 10-Oct-2021.) |
Ref | Expression |
---|---|
nexdv.1 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
nexdv | ⊢ (𝜑 → ¬ ∃𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1914 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | nexdv.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
3 | 1, 2 | nexdh 1869 | 1 ⊢ (𝜑 → ¬ ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: sbc2or 3753 csbopab 5517 relimasn 6041 csbiota 6494 0mpo0 7445 1sdom2dom 9198 canthwdom 9522 cfsuc 10200 ssfin4 10253 konigthlem 10511 axunndlem1 10538 canthnum 10592 canthwe 10594 pwfseq 10607 tskuni 10726 ptcmplem4 23422 lgsquadlem3 26746 umgredgnlp 28140 iswspthsnon 28843 acycgr0v 33782 acycgr2v 33784 prclisacycgr 33785 dfrdg4 34565 |
Copyright terms: Public domain | W3C validator |