![]() |
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 2948 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
3 | 2 | con2i 136 | 1 ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1631 ≠ wne 2943 |
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 2944 |
This theorem is referenced by: rzal 4214 difsnb 4472 dtrucor2 5029 kmlem6 9179 winainflem 9717 0npi 9906 0npr 10016 0nsr 10102 1div0 10888 rexmul 12306 rennim 14187 mrissmrcd 16508 prmirred 20058 pthaus 21662 rplogsumlem2 25395 pntrlog2bndlem4 25490 pntrlog2bndlem5 25491 1div0apr 27666 bnj1311 31430 subfacp1lem6 31505 bj-dtrucor2v 33137 itg2addnclem3 33795 cdleme31id 36203 sdrgacs 38297 rzalf 39698 jumpncnp 40629 fourierswlem 40964 |
Copyright terms: Public domain | W3C validator |