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

Theorem necon2bi 2969
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 2943 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32con2i 139 1 (𝐴 = 𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wne 2938
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 206  df-ne 2939
This theorem is referenced by:  rzalALT  4508  difsnb  4808  dtrucor2  5369  omeulem1  8584  kmlem6  10152  winainflem  10690  0npi  10879  0npr  10989  0nsr  11076  1div0  11877  rexmul  13254  rennim  15190  mrissmrcd  17588  sdrgacs  20560  prmirred  21245  pthaus  23362  rplogsumlem2  27224  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  1div0apr  29988  bnj1311  34333  subfacp1lem6  34474  bj-dtrucor2v  35998  itg2addnclem3  36844  cdleme31id  39568  rzalf  44003  jumpncnp  44912  fourierswlem  45244
  Copyright terms: Public domain W3C validator