![]() |
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 1953 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | nexdv.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
3 | 1, 2 | nexdh 1910 | 1 ⊢ (𝜑 → ¬ ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∃wex 1823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 |
This theorem depends on definitions: df-bi 199 df-ex 1824 |
This theorem is referenced by: sbc2or 3661 csbopab 5245 relimasn 5742 csbiota 6128 canthwdom 8773 cfsuc 9414 ssfin4 9467 konigthlem 9725 axunndlem1 9752 canthnum 9806 canthwe 9808 pwfseq 9821 tskuni 9940 ptcmplem4 22267 lgsquadlem3 25559 umgredgnlp 26496 dfrdg4 32647 |
Copyright terms: Public domain | W3C validator |