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

Theorem necon2bi 2598
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 2568 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 114 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2552
This theorem is referenced by:  necon4i  2612  minel  3628  rzal  3674  difsnb  3885  dtrucor2  4341  reusv7OLD  4677  riotaundb  6529  kmlem6  7970  winainflem  8503  0npi  8694  0npr  8804  0nsr  8889  renfdisj  9073  1div0  9613  rexmul  10784  rennim  11973  mrissmrcd  13794  prmirred  16700  pthaus  17593  rplogsumlem2  21048  pntrlog2bndlem4  21143  pntrlog2bndlem5  21144  1div0apr  21612  subfacp1lem6  24652  sdrgacs  27180  rzalf  27358  bnj1311  28733  cdleme31id  30510
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 178  df-ne 2554
  Copyright terms: Public domain W3C validator