![]() |
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 2942 | . . 3 ⊢ (¬ 𝐶 ≠ 𝐷 ↔ 𝐶 = 𝐷) | |
3 | 1, 2 | imbitrrdi 252 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝐶 ≠ 𝐷)) |
4 | 3 | necon4ad 2957 | 1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1537 ≠ wne 2938 |
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 2939 |
This theorem is referenced by: disji 5133 mul02lem2 11436 mhpmulcl 22171 xblss2ps 24427 xblss2 24428 lgsne0 27394 h1datomi 31610 eigorthi 31866 disjif 32598 lineintmo 36139 poimirlem6 37613 poimirlem7 37614 2llnmat 39507 2lnat 39767 tendospcanN 41006 dihmeetlem13N 41302 dochkrshp 41369 remul02 42412 remul01 42414 sn-0tie0 42446 |
Copyright terms: Public domain | W3C validator |