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

Theorem necon2bi 3017
 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 2992 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32con2i 141 1 (𝐴 = 𝐵 → ¬ 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987 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 210  df-ne 2988 This theorem is referenced by:  rzal  4411  difsnb  4699  dtrucor2  5239  omeulem1  8194  kmlem6  9569  winainflem  10107  0npi  10296  0npr  10406  0nsr  10493  1div0  11291  rexmul  12655  rennim  14593  mrissmrcd  16906  sdrgacs  19577  prmirred  20193  pthaus  22253  rplogsumlem2  26079  pntrlog2bndlem4  26174  pntrlog2bndlem5  26175  1div0apr  28263  bnj1311  32421  subfacp1lem6  32560  bj-dtrucor2v  34274  itg2addnclem3  35129  cdleme31id  37709  rzalf  41689  jumpncnp  42583  fourierswlem  42915
 Copyright terms: Public domain W3C validator