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 2957 | . 2 ⊢ (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴 ≠ 𝐵)) |
3 | nne 2945 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
4 | 2, 3 | syl6ib 254 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1543 ≠ wne 2941 |
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 2942 |
This theorem is referenced by: oa00 8307 map0g 8585 epfrs 9371 fin23lem24 9960 abs00 14877 oddvds 18963 isabvd 19880 01eq0ring 20334 uvcf1 20778 lindff1 20806 hausnei2 22274 dfconn2 22340 hausflimi 22901 hauspwpwf1 22908 cxpeq0 25590 his6 29204 fnpreimac 30752 lkreqN 36947 ltrnideq 37952 hdmapip0 39692 sticksstones2 39854 isdomn4 39923 rpnnen3 40585 |
Copyright terms: Public domain | W3C validator |