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  4823  kmlem6  8838  winainflem  9372  0npi  9561  0npr  9671  0nsr  9757  1div0  10538  rexmul  11933  rennim  13776  mrissmrcd  16072  prmirred  19610  pthaus  21199  rplogsumlem2  24919  pntrlog2bndlem4  25014  pntrlog2bndlem5  25015  1div0apr  26510  bnj1311  30140  subfacp1lem6  30215  bj-dtrucor2v  31783  itg2addnclem3  32427  cdleme31id  34494  sdrgacs  36584  rzalf  37993  jumpncnp  38578  fourierswlem  38917  av-numclwwlkffin0  41505
  Copyright terms: Public domain W3C validator