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

Theorem necon3abii 2633
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 2603 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abii.1 . 2  |-  ( A  =  B  <->  ph )
31, 2xchbinx 303 1  |-  ( A  =/=  B  <->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178    = wceq 1653    =/= wne 2601
This theorem is referenced by:  necon3bbii  2634  necon3bii  2635  nesym  2642  n0f  3638  rankxplim3  7807  rankxpsuc  7808  dflt2  10743  gcd0id  13025  ballotlemi1  24762  axlowdimlem13  25895  filnetlem4  26412  pellex  26900  dihatlat  32194
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator