![]() |
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 2942 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | imbitrdi 250 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷)) |
4 | 3 | necon2ad 2956 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ 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 206 df-ne 2942 |
This theorem is referenced by: map0g 8878 cantnf 9688 hashprg 14355 bcthlem5 24845 deg1ldgn 25611 cxpeq0 26186 lfgrn1cycl 29059 uspgrn2crct 29062 poimirlem17 36505 poimirlem20 36508 poimirlem22 36510 poimirlem27 36515 islshpat 37887 cdleme18b 39163 cdlemh 39688 prjspner1 41368 |
Copyright terms: Public domain | W3C validator |