![]() |
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 3003 | . 2 ⊢ (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴 ≠ 𝐵)) |
3 | nne 2991 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
4 | 2, 3 | syl6ib 254 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1538 ≠ wne 2987 |
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 2988 |
This theorem is referenced by: oa00 8168 map0g 8431 epfrs 9157 fin23lem24 9733 abs00 14641 oddvds 18667 isabvd 19584 01eq0ring 20038 uvcf1 20481 lindff1 20509 hausnei2 21958 dfconn2 22024 hausflimi 22585 hauspwpwf1 22592 cxpeq0 25269 his6 28882 fnpreimac 30434 lkreqN 36466 ltrnideq 37471 hdmapip0 39211 rpnnen3 39973 |
Copyright terms: Public domain | W3C validator |