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 2782 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | syl6ib 240 | . 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝐶 = 𝐷)) |
4 | 3 | necon2ad 2797 | 1 ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1475 ≠ wne 2780 |
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 196 df-ne 2782 |
This theorem is referenced by: map0g 7783 cantnf 8473 hashprg 13043 hashprgOLD 13044 bcthlem5 22933 deg1ldgn 23657 cxpeq0 24224 poimirlem17 32596 poimirlem20 32599 poimirlem22 32601 poimirlem27 32606 islshpat 33322 cdleme18b 34597 cdlemh 35123 lfgrn1cycl 41008 uspgrn2crct 41011 |
Copyright terms: Public domain | W3C validator |