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 2787 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
3 | 2 | con2i 133 | 1 ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1475 ≠ wne 2780 |
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 196 df-ne 2782 |
This theorem is referenced by: minelOLD 3986 rzal 4025 difsnb 4278 dtrucor2 4828 kmlem6 8860 winainflem 9394 0npi 9583 0npr 9693 0nsr 9779 1div0 10565 rexmul 11973 rennim 13827 mrissmrcd 16123 prmirred 19662 pthaus 21251 rplogsumlem2 24974 pntrlog2bndlem4 25069 pntrlog2bndlem5 25070 1div0apr 26716 bnj1311 30346 subfacp1lem6 30421 bj-dtrucor2v 31989 itg2addnclem3 32633 cdleme31id 34700 sdrgacs 36790 rzalf 38199 jumpncnp 38784 fourierswlem 39123 av-numclwwlkffin0 41513 |
Copyright terms: Public domain | W3C validator |