MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon2bi Structured version   Visualization version   GIF version

Theorem necon2bi 2812
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
Hypothesis
Ref Expression
necon2bi.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
necon2bi (𝐴 = 𝐵 → ¬ 𝜑)

Proof of Theorem necon2bi
StepHypRef Expression
1 necon2bi.1 . . 3 (𝜑𝐴𝐵)
21neneqd 2787 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32con2i 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