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 1541  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 206  df-ne 2941
This theorem is referenced by:  rzalALT  4508  difsnb  4808  dtrucor2  5369  omeulem1  8578  kmlem6  10146  winainflem  10684  0npi  10873  0npr  10983  0nsr  11070  1div0  11869  rexmul  13246  rennim  15182  mrissmrcd  17580  sdrgacs  20409  prmirred  21035  pthaus  23133  rplogsumlem2  26977  pntrlog2bndlem4  27072  pntrlog2bndlem5  27073  1div0apr  29710  bnj1311  34023  subfacp1lem6  34164  bj-dtrucor2v  35683  itg2addnclem3  36529  cdleme31id  39253  rzalf  43686  jumpncnp  44600  fourierswlem  44932
  Copyright terms: Public domain W3C validator