Metamath Proof Explorer
Description: Assuming a, not b, and a implies b, there exists a proof that a is
false.) (Contributed by Jarvin Udandy, 29-Aug-2016)
|
|
Ref |
Expression |
|
Hypotheses |
conimpfalt.1 |
|
|
|
conimpfalt.2 |
|
|
|
conimpfalt.3 |
|
|
Assertion |
conimpfalt |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
conimpfalt.1 |
|
2 |
|
conimpfalt.2 |
|
3 |
|
conimpfalt.3 |
|
4 |
3 2
|
aibnbaif |
|