![]() |
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 1906 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | nexdv.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
3 | 1, 2 | nexdh 1861 | 1 ⊢ (𝜑 → ¬ ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∃wex 1774 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-ex 1775 |
This theorem is referenced by: sbc2or 3785 csbopab 5561 relimasn 6094 csbiota 6547 0mpo0 7508 1sdom2dom 9281 canthwdom 9622 cfsuc 10300 ssfin4 10353 konigthlem 10611 axunndlem1 10638 canthnum 10692 canthwe 10694 pwfseq 10707 tskuni 10826 ptcmplem4 24050 lgsquadlem3 27411 umgredgnlp 29083 iswspthsnon 29790 acycgr0v 34976 acycgr2v 34978 prclisacycgr 34979 dfrdg4 35775 |
Copyright terms: Public domain | W3C validator |