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 3035 | . 2 ⊢ (𝜑 → (𝐶 = 𝐷 → ¬ 𝐴 ≠ 𝐵)) |
3 | nne 3023 | . 2 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
4 | 2, 3 | syl6ib 253 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1536 ≠ wne 3019 |
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 209 df-ne 3020 |
This theorem is referenced by: oa00 8188 map0g 8451 epfrs 9176 fin23lem24 9747 abs00 14652 oddvds 18678 isabvd 19594 01eq0ring 20048 uvcf1 20939 lindff1 20967 hausnei2 21964 dfconn2 22030 hausflimi 22591 hauspwpwf1 22598 cxpeq0 25264 his6 28879 fnpreimac 30419 lkreqN 36310 ltrnideq 37315 hdmapip0 39055 rpnnen3 39635 |
Copyright terms: Public domain | W3C validator |