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

Theorem necon3abii 2489
Description: Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
Hypothesis
Ref Expression
necon3abii.1  |-  ( A  =  B  <->  ph )
Assertion
Ref Expression
necon3abii  |-  ( A  =/=  B  <->  -.  ph )

Proof of Theorem necon3abii
StepHypRef Expression
1 df-ne 2461 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abii.1 . 2  |-  ( A  =  B  <->  ph )
31, 2xchbinx 301 1  |-  ( A  =/=  B  <->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    = wceq 1632    =/= wne 2459
This theorem is referenced by:  necon3bbii  2490  necon3bii  2491  n0f  3476  rankxplim3  7567  rankxpsuc  7568  dflt2  10498  gcd0id  12718  ballotlemi1  23077  xrge0iifhom  23334  axlowdimlem13  24654  filnetlem4  26433  pellex  27023  wlkntrllem2  28346  dihatlat  32146
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