Metamath Proof Explorer
Description: An inference for negation elimination. (Contributed by Giovanni
Mascellani, 24-May-2019)
|
|
Ref |
Expression |
|
Hypotheses |
negel.1 |
|
|
|
negel.2 |
|
|
Assertion |
negel |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
negel.1 |
|
2 |
|
negel.2 |
|
3 |
1
|
adantl |
|
4 |
2
|
adantr |
|
5 |
3 4
|
pm2.21fal |
|