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

Theorem necon3abii 2684
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 2620 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abii.1 . 2  |-  ( A  =  B  <->  ph )
31, 2xchbinx 311 1  |-  ( A  =/=  B  <->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187    = wceq 1437    =/= wne 2618
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 188  df-ne 2620
This theorem is referenced by:  necon3bbii  2685  necon3bii  2692  nesym  2696  n0f  3770  xpimasn  5298  rankxplim3  8354  rankxpsuc  8355  dflt2  11448  gcd0id  14475  lcmfunsnlem2  14601  axlowdimlem13  24971  filnetlem4  31030  dihatlat  34821  pellex  35599  nev  36220  ldepspr  39540
  Copyright terms: Public domain W3C validator