![]() |
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 2933 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | syl6ib 241 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷)) |
4 | 3 | necon2ad 2947 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1632 ≠ wne 2932 |
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 197 df-ne 2933 |
This theorem is referenced by: map0g 8065 cantnf 8765 hashprg 13394 hashprgOLD 13395 bcthlem5 23345 deg1ldgn 24072 cxpeq0 24644 lfgrn1cycl 26929 uspgrn2crct 26932 poimirlem17 33757 poimirlem20 33760 poimirlem22 33762 poimirlem27 33767 islshpat 34825 cdleme18b 36100 cdlemh 36625 |
Copyright terms: Public domain | W3C validator |