Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007)
Ref | Expression | ||
---|---|---|---|
Hypothesis | necon3abid.1 | |
|
Assertion | necon3abid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3abid.1 | |
|
2 | df-ne | |
|
3 | 1 | notbid | |
4 | 2 3 | bitrid | |