![]() |
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 250 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1541 ≠ 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 206 df-ne 2941 |
This theorem is referenced by: oa00 8561 map0g 8880 epfrs 9728 fin23lem24 10319 abs00 15240 oddvds 19456 01eq0ringOLD 20420 isabvd 20571 isdomn4 21118 uvcf1 21566 lindff1 21594 hausnei2 23077 dfconn2 23143 hausflimi 23704 hauspwpwf1 23711 cxpeq0 26410 his6 30607 fnpreimac 32151 deg1le0eq0 32917 lkreqN 38343 ltrnideq 39349 hdmapip0 41089 sticksstones2 41269 rpnnen3 42073 |
Copyright terms: Public domain | W3C validator |