| 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 2956 | . 2 ⊢ (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴 ≠ 𝐵)) |
| 3 | nne 2944 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
| 4 | 2, 3 | imbitrdi 251 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ wne 2940 |
| 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 2941 |
| This theorem is referenced by: oa00 8597 map0g 8924 epfrs 9771 fin23lem24 10362 abs00 15328 oddvds 19565 01eq0ringOLD 20531 isdomn4 20716 isabvd 20813 uvcf1 21812 lindff1 21840 hausnei2 23361 dfconn2 23427 hausflimi 23988 hauspwpwf1 23995 cxpeq0 26720 his6 31118 fnpreimac 32681 deg1le0eq0 33598 lkreqN 39171 ltrnideq 40177 hdmapip0 41917 sticksstones2 42148 unitscyglem4 42199 rpnnen3 43044 |
| Copyright terms: Public domain | W3C validator |