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 3020 | . . 3 ⊢ (¬ 𝐶 ≠ 𝐷 ↔ 𝐶 = 𝐷) | |
3 | 1, 2 | syl6ibr 254 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝐶 ≠ 𝐷)) |
4 | 3 | necon4ad 3035 | 1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1537 ≠ wne 3016 |
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 209 df-ne 3017 |
This theorem is referenced by: disji 5049 mul02lem2 10817 xblss2ps 23011 xblss2 23012 lgsne0 25911 h1datomi 29358 eigorthi 29614 disjif 30328 lineintmo 33618 poimirlem6 34913 poimirlem7 34914 2llnmat 36675 2lnat 36935 tendospcanN 38174 dihmeetlem13N 38470 dochkrshp 38537 remul02 39255 remul01 39257 |
Copyright terms: Public domain | W3C validator |