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 2945 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
3 | 2 | con2i 141 | 1 ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1543 ≠ wne 2940 |
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 210 df-ne 2941 |
This theorem is referenced by: rzalALT 4421 difsnb 4719 dtrucor2 5265 omeulem1 8310 kmlem6 9769 winainflem 10307 0npi 10496 0npr 10606 0nsr 10693 1div0 11491 rexmul 12861 rennim 14802 mrissmrcd 17143 sdrgacs 19845 prmirred 20461 pthaus 22535 rplogsumlem2 26366 pntrlog2bndlem4 26461 pntrlog2bndlem5 26462 1div0apr 28551 bnj1311 32717 subfacp1lem6 32860 bj-dtrucor2v 34737 itg2addnclem3 35567 cdleme31id 38145 rzalf 42233 jumpncnp 43114 fourierswlem 43446 |
Copyright terms: Public domain | W3C validator |