![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon2d | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.) |
Ref | Expression |
---|---|
necon2d.1 | ⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)) |
Ref | Expression |
---|---|
necon2d | ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon2d.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)) | |
2 | df-ne 2945 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | syl6ib 251 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷)) |
4 | 3 | necon2ad 2959 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ wne 2944 |
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 2945 |
This theorem is referenced by: map0g 8829 cantnf 9636 hashprg 14302 bcthlem5 24708 deg1ldgn 25474 cxpeq0 26049 lfgrn1cycl 28792 uspgrn2crct 28795 poimirlem17 36124 poimirlem20 36127 poimirlem22 36129 poimirlem27 36134 islshpat 37508 cdleme18b 38784 cdlemh 39309 prjspner1 40993 |
Copyright terms: Public domain | W3C validator |