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 253 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝐶 ≠ 𝐷)) |
4 | 3 | necon4ad 3035 | 1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ≠ 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 208 df-ne 3017 |
This theorem is referenced by: disji 5041 mul02lem2 10806 xblss2ps 22940 xblss2 22941 lgsne0 25839 h1datomi 29286 eigorthi 29542 disjif 30257 lineintmo 33516 poimirlem6 34780 poimirlem7 34781 2llnmat 36542 2lnat 36802 tendospcanN 38041 dihmeetlem13N 38337 dochkrshp 38404 remul02 39115 remul01 39117 |
Copyright terms: Public domain | W3C validator |