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

Theorem necon3abii 2476
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 2448 . 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 1623    =/= wne 2446
This theorem is referenced by:  necon3bbii  2477  necon3bii  2478  n0f  3463  rankxplim3  7551  rankxpsuc  7552  dflt2  10482  gcd0id  12702  ballotlemi1  23061  xrge0iifhom  23319  axlowdimlem13  24582  filnetlem4  26330  pellex  26920  dihatlat  31524
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 2448
  Copyright terms: Public domain W3C validator