| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > necon1d | Structured version Visualization version GIF version | ||
| Description: Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
| Ref | Expression |
|---|---|
| necon1d.1 | ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)) |
| Ref | Expression |
|---|---|
| necon1d | ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | necon1d.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷)) | |
| 2 | nne 2944 | . . 3 ⊢ (¬ 𝐶 ≠ 𝐷 ↔ 𝐶 = 𝐷) | |
| 3 | 1, 2 | imbitrrdi 252 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝐶 ≠ 𝐷)) |
| 4 | 3 | necon4ad 2959 | 1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ wne 2940 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-ne 2941 |
| This theorem is referenced by: disji 5128 mul02lem2 11438 mhpmulcl 22153 xblss2ps 24411 xblss2 24412 lgsne0 27379 h1datomi 31600 eigorthi 31856 disjif 32591 lineintmo 36158 poimirlem6 37633 poimirlem7 37634 2llnmat 39526 2lnat 39786 tendospcanN 41025 dihmeetlem13N 41321 dochkrshp 41388 remul02 42435 remul01 42437 sn-0tie0 42469 oppcthinendcALT 49090 |
| Copyright terms: Public domain | W3C validator |