![]() |
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 2939 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | imbitrdi 250 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷)) |
4 | 3 | necon2ad 2953 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ≠ wne 2938 |
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 2939 |
This theorem is referenced by: map0g 8880 cantnf 9690 hashprg 14359 bcthlem5 25076 deg1ldgn 25846 cxpeq0 26422 lfgrn1cycl 29326 uspgrn2crct 29329 poimirlem17 36808 poimirlem20 36811 poimirlem22 36813 poimirlem27 36818 islshpat 38190 cdleme18b 39466 cdlemh 39991 prjspner1 41670 |
Copyright terms: Public domain | W3C validator |