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

Theorem necon2bi 2821
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 2796 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32con2i 134 1 (𝐴 = 𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1481  wne 2791
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 197  df-ne 2792
This theorem is referenced by:  minelOLD  4025  rzal  4064  difsnb  4328  dtrucor2  4892  kmlem6  8962  winainflem  9500  0npi  9689  0npr  9799  0nsr  9885  1div0  10671  rexmul  12086  rennim  13960  mrissmrcd  16281  prmirred  19824  pthaus  21422  rplogsumlem2  25155  pntrlog2bndlem4  25250  pntrlog2bndlem5  25251  numclwwlkffin0  27187  1div0apr  27294  bnj1311  31066  subfacp1lem6  31141  bj-dtrucor2v  32776  itg2addnclem3  33434  cdleme31id  35501  sdrgacs  37590  rzalf  38996  jumpncnp  39874  fourierswlem  40210
  Copyright terms: Public domain W3C validator