Description: Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008) (Proof shortened by Wolf Lammen, 24-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | necon4abid.1 | |
|
Assertion | necon4abid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon4abid.1 | |
|
2 | notnotb | |
|
3 | 1 | necon1bbid | |
4 | 2 3 | bitr2id | |