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

Theorem necon2bi 2505
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 2475 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 112 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  necon4i  2519  minel  3523  rzal  3568  difsnb  3773  dtrucor2  4225  reusv7OLD  4562  riotaundb  6362  fofinf1o  7153  kmlem6  7797  winainflem  8331  0npi  8522  0npr  8632  0nsr  8717  renfdisj  8901  1div0  9441  rexmul  10607  xrsupss  10643  rennim  11740  mrissmrcd  13558  prmirred  16464  pthaus  17348  rplogsumlem2  20650  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  1div0apr  20857  subfacp1lem6  23731  sdrgacs  27612  rzalf  27791  bnj1311  29370  cdleme31id  31205
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 2461
  Copyright terms: Public domain W3C validator