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

Theorem necon2bi 2525
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
Hypothesis
Ref Expression
necon2bi.1  |-  ( ph  ->  A  =/=  B )
Assertion
Ref Expression
necon2bi  |-  ( A  =  B  ->  -.  ph )

Proof of Theorem necon2bi
StepHypRef Expression
1 necon2bi.1 . . 3  |-  ( ph  ->  A  =/=  B )
21neneqd 2495 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 112 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1633    =/= wne 2479
This theorem is referenced by:  necon4i  2539  minel  3544  rzal  3589  difsnb  3794  dtrucor2  4246  reusv7OLD  4583  riotaundb  6388  fofinf1o  7182  kmlem6  7826  winainflem  8360  0npi  8551  0npr  8661  0nsr  8746  renfdisj  8930  1div0  9470  rexmul  10638  xrsupss  10674  rennim  11771  mrissmrcd  13591  prmirred  16504  pthaus  17388  rplogsumlem2  20687  pntrlog2bndlem4  20782  pntrlog2bndlem5  20783  1div0apr  20894  subfacp1lem6  24000  sdrgacs  26657  rzalf  26836  bnj1311  28565  cdleme31id  30401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2481
  Copyright terms: Public domain W3C validator