Description: Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007) (Proof shortened by Wolf Lammen, 24-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | necon1bbii.1 | |
|
Assertion | necon1bbii | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon1bbii.1 | |
|
2 | nne | |
|
3 | 2 1 | xchnxbi | |