| 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 1540 ≠ 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 207 df-ne 2941 |
| This theorem is referenced by: rzalALT 4510 difsnb 4806 dtrucor2 5372 omeulem1 8620 kmlem6 10196 winainflem 10733 0npi 10922 0npr 11032 0nsr 11119 1div0OLD 11923 rexmul 13313 rennim 15278 mrissmrcd 17683 sdrgacs 20802 prmirred 21485 pthaus 23646 rplogsumlem2 27529 pntrlog2bndlem4 27624 pntrlog2bndlem5 27625 1div0apr 30487 bnj1311 35038 subfacp1lem6 35190 bj-dtrucor2v 36818 itg2addnclem3 37680 cdleme31id 40396 rzalf 45022 jumpncnp 45913 fourierswlem 46245 |
| Copyright terms: Public domain | W3C validator |