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

Theorem necon3abii 2636
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 2606 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abii.1 . 2  |-  ( A  =  B  <->  ph )
31, 2xchbinx 310 1  |-  ( A  =/=  B  <->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1364    =/= wne 2604
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 2606
This theorem is referenced by:  necon3bbii  2637  necon3bii  2638  nesym  2645  n0f  3642  xpimasn  5280  rankxplim3  8084  rankxpsuc  8085  dflt2  11121  gcd0id  13703  axlowdimlem13  23119  ballotlemi1  26799  filnetlem4  28511  pellex  29085  ldepspr  30831  dihatlat  34667
  Copyright terms: Public domain W3C validator