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

Theorem necon2bi 2704
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 2669 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 120 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1379    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2664
This theorem is referenced by:  necon4iOLD  2712  minel  3882  rzal  3929  difsnb  4169  reusv7OLD  4659  dtrucor2  4681  kmlem6  8531  winainflem  9067  0npi  9256  0npr  9366  0nsr  9452  renfdisj  9643  1div0  10204  rexmul  11459  rennim  13029  mrissmrcd  14888  prmirred  18289  prmirredOLD  18292  pthaus  19871  rplogsumlem2  23395  pntrlog2bndlem4  23490  pntrlog2bndlem5  23491  1div0apr  24849  subfacp1lem6  28266  itg2addnclem3  29643  sdrgacs  30755  rzalf  30970  jumpncnp  31237  fourierswlem  31531  bnj1311  33159  bj-dtrucor2v  33468  cdleme31id  35190
  Copyright terms: Public domain W3C validator