|   | 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 2940 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
| 3 | 1, 2 | imbitrdi 251 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷)) | 
| 4 | 3 | necon2ad 2954 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ≠ wne 2939 | 
| 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 207 df-ne 2940 | 
| This theorem is referenced by: map0g 8925 cantnf 9734 hashprg 14435 bcthlem5 25363 deg1ldgn 26133 cxpeq0 26721 lfgrn1cycl 29826 uspgrn2crct 29829 poimirlem17 37645 poimirlem20 37648 poimirlem22 37650 poimirlem27 37655 islshpat 39019 cdleme18b 40295 cdlemh 40820 prjspner1 42641 | 
| Copyright terms: Public domain | W3C validator |