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

Theorem necon2bi 2644
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 2614 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 114 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  necon4i  2658  minel  3675  rzal  3721  difsnb  3932  dtrucor2  4390  reusv7OLD  4727  riotaundb  6583  kmlem6  8027  winainflem  8560  0npi  8751  0npr  8861  0nsr  8946  renfdisj  9130  1div0  9671  rexmul  10842  rennim  12036  mrissmrcd  13857  prmirred  16767  pthaus  17662  rplogsumlem2  21171  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  1div0apr  21754  subfacp1lem6  24863  itg2addnclem3  26248  sdrgacs  27467  rzalf  27645  bnj1311  29320  cdleme31id  31118
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 2600
  Copyright terms: Public domain W3C validator