Metamath Proof Explorer
Description: Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016)
|
|
Ref |
Expression |
|
Hypotheses |
nexd.1 |
⊢ Ⅎ 𝑥 𝜑 |
|
|
nexd.2 |
⊢ ( 𝜑 → ¬ 𝜓 ) |
|
Assertion |
nexd |
⊢ ( 𝜑 → ¬ ∃ 𝑥 𝜓 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nexd.1 |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
nexd.2 |
⊢ ( 𝜑 → ¬ 𝜓 ) |
3 |
1
|
nf5ri |
⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) |
4 |
3 2
|
nexdh |
⊢ ( 𝜑 → ¬ ∃ 𝑥 𝜓 ) |