![]() |
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 2827 | . . 3 ⊢ (¬ 𝐶 ≠ 𝐷 ↔ 𝐶 = 𝐷) | |
3 | 1, 2 | syl6ibr 242 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝐶 ≠ 𝐷)) |
4 | 3 | necon4ad 2842 | 1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1523 ≠ wne 2823 |
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 197 df-ne 2824 |
This theorem is referenced by: disji 4669 mul02lem2 10251 xblss2ps 22253 xblss2 22254 lgsne0 25105 h1datomi 28568 eigorthi 28824 disjif 29517 lineintmo 32389 poimirlem6 33545 poimirlem7 33546 2llnmat 35128 2lnat 35388 tendospcanN 36629 dihmeetlem13N 36925 dochkrshp 36992 |
Copyright terms: Public domain | W3C validator |