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

Theorem necon2bi 2971
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 2945 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32con2i 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