| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > necon4d | Structured version Visualization version GIF version | ||
| Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
| Ref | Expression |
|---|---|
| necon4d.1 | ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷)) |
| Ref | Expression |
|---|---|
| necon4d | ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | necon4d.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷)) | |
| 2 | 1 | necon2bd 2976 | . 2 ⊢ (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴 ≠ 𝐵)) |
| 3 | nne 2964 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
| 4 | 2, 3 | imbitrdi 254 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1563 ≠ wne 2960 |
| 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 210 df-ne 2961 |
| This theorem is referenced by: oa00 8532 map0g 8870 epfrs 9688 fin23lem24 10294 abs00 15328 oddvds 19605 01eq0ringOLD 20603 isdomn4 20788 isabvd 20881 uvcf1 21899 lindff1 21927 hausnei2 23467 dfconn2 23533 hausflimi 24094 hauspwpwf1 24101 cxpeq0 26797 his6 31356 fnpreimac 32923 deg1le0eq0 33775 lkreqN 39801 ltrnideq 40806 hdmapip0 42546 sticksstones2 42771 unitscyglem4 42822 rpnnen3 43616 |
| Copyright terms: Public domain | W3C validator |