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 1827 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | nexdv.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
3 | 1, 2 | nexdh 1779 | 1 ⊢ (𝜑 → ¬ ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: sbc2or 3411 csbopab 4932 relimasn 5407 csbiota 5797 canthwdom 8367 cfsuc 8962 ssfin4 9015 konigthlem 9269 axunndlem1 9296 canthnum 9350 canthwe 9352 pwfseq 9365 tskuni 9484 ptcmplem4 21669 lgsquadlem3 24907 umgredgnlp 25818 dfrdg4 31228 |
Copyright terms: Public domain | W3C validator |