Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon2bi | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.) |
Ref | Expression |
---|---|
necon2bi.1 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
Ref | Expression |
---|---|
necon2bi | ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon2bi.1 | . . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
2 | 1 | neneqd 3021 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
3 | 2 | con2i 141 | 1 ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: rzal 4451 difsnb 4733 dtrucor2 5265 omeulem1 8198 kmlem6 9570 winainflem 10104 0npi 10293 0npr 10403 0nsr 10490 1div0 11288 rexmul 12654 rennim 14588 mrissmrcd 16901 sdrgacs 19511 prmirred 20572 pthaus 22176 rplogsumlem2 25989 pntrlog2bndlem4 26084 pntrlog2bndlem5 26085 1div0apr 28175 bnj1311 32194 subfacp1lem6 32330 bj-dtrucor2v 34038 itg2addnclem3 34827 cdleme31id 37412 rzalf 41154 jumpncnp 42061 fourierswlem 42396 |
Copyright terms: Public domain | W3C validator |