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

Theorem necon2bi 2492
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 2462 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 112 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  necon4i  2506  minel  3510  rzal  3555  difsneq  3757  dtrucor2  4209  reusv7OLD  4546  riotaundb  6346  fofinf1o  7137  kmlem6  7781  winainflem  8315  0npi  8506  0npr  8616  0nsr  8701  renfdisj  8885  1div0  9425  rexmul  10591  xrsupss  10627  rennim  11724  mrissmrcd  13542  prmirred  16448  pthaus  17332  rplogsumlem2  20634  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  1div0apr  20841  subfacp1lem6  23716  sdrgacs  27509  rzalf  27688  bnj1311  29054  cdleme31id  30583
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 2448
  Copyright terms: Public domain W3C validator