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

Theorem necon3abii 2717
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 2654 . 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 1395    =/= wne 2652
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 2654
This theorem is referenced by:  necon3bbii  2718  necon3bii  2725  nesym  2729  n0f  3802  xpimasn  5459  rankxplim3  8316  rankxpsuc  8317  dflt2  11379  gcd0id  14172  axlowdimlem13  24383  filnetlem4  30361  pellex  30933  ldepspr  33176  dihatlat  37162  nev  37892
  Copyright terms: Public domain W3C validator