Metamath Proof Explorer
Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013) (Proof shortened by Wolf Lammen, 11-Apr-2024)
|
|
Ref |
Expression |
|
Hypotheses |
2falsed.1 |
|
|
|
2falsed.2 |
|
|
Assertion |
2falsed |
|
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
2falsed.1 |
|
| 2 |
|
2falsed.2 |
|
| 3 |
1 2
|
2thd |
|
| 4 |
3
|
con4bid |
|