![]() |
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 139 | 1 ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1541 ≠ 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 206 df-ne 2941 |
This theorem is referenced by: rzalALT 4508 difsnb 4808 dtrucor2 5369 omeulem1 8578 kmlem6 10146 winainflem 10684 0npi 10873 0npr 10983 0nsr 11070 1div0 11869 rexmul 13246 rennim 15182 mrissmrcd 17580 sdrgacs 20409 prmirred 21035 pthaus 23133 rplogsumlem2 26977 pntrlog2bndlem4 27072 pntrlog2bndlem5 27073 1div0apr 29710 bnj1311 34023 subfacp1lem6 34164 bj-dtrucor2v 35683 itg2addnclem3 36529 cdleme31id 39253 rzalf 43686 jumpncnp 44600 fourierswlem 44932 |
Copyright terms: Public domain | W3C validator |