Description: Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008) (Proof shortened by Andrew Salmon, 25-May-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | necon1d.1 | |- ( ph -> ( A =/= B -> C = D ) ) |
|
| Assertion | necon1d | |- ( ph -> ( C =/= D -> A = B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | necon1d.1 | |- ( ph -> ( A =/= B -> C = D ) ) |
|
| 2 | nne | |- ( -. C =/= D <-> C = D ) |
|
| 3 | 1 2 | syl6ibr | |- ( ph -> ( A =/= B -> -. C =/= D ) ) |
| 4 | 3 | necon4ad | |- ( ph -> ( C =/= D -> A = B ) ) |