Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006) (Proof shortened by Wolf Lammen, 22-Nov-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | necon3i.1 | |- ( A = B -> C = D ) |
|
| Assertion | necon3i | |- ( C =/= D -> A =/= B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | necon3i.1 | |- ( A = B -> C = D ) |
|
| 2 | 1 | necon3ai | |- ( C =/= D -> -. A = B ) |
| 3 | 2 | neqned | |- ( C =/= D -> A =/= B ) |