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

Theorem necon3abii 2638
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 2608 . 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 1369    =/= wne 2606
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 2608
This theorem is referenced by:  necon3bbii  2639  necon3bii  2640  nesym  2647  n0f  3645  xpimasn  5283  rankxplim3  8088  rankxpsuc  8089  dflt2  11125  gcd0id  13707  axlowdimlem13  23200  ballotlemi1  26885  filnetlem4  28602  pellex  29176  ldepspr  31007  dihatlat  34979
  Copyright terms: Public domain W3C validator