Metamath Proof Explorer
Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005) (Proof shortened by Andrew Salmon, 25-May-2011)
|
|
Ref |
Expression |
|
Hypothesis |
necon3bid.1 |
|
|
Assertion |
necon3bid |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
necon3bid.1 |
|
2 |
|
df-ne |
|
3 |
1
|
necon3bbid |
|
4 |
2 3
|
bitrid |
|