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

Theorem necon3abii 2976
Description: Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
Hypothesis
Ref Expression
necon3abii.1 (𝐴 = 𝐵𝜑)
Assertion
Ref Expression
necon3abii (𝐴𝐵 ↔ ¬ 𝜑)

Proof of Theorem necon3abii
StepHypRef Expression
1 df-ne 2930 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abii.1 . 2 (𝐴 = 𝐵𝜑)
31, 2xchbinx 333 1 (𝐴𝐵 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1533  wne 2929
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 206  df-ne 2930
This theorem is referenced by:  necon3bbii  2977  necon3bii  2982  nesym  2986  rabn0  4387  dffr6  5636  xpimasn  6191  rankxplim3  9906  rankxpsuc  9907  dflt2  13162  gcd0id  16497  lcmfunsnlem2  16614  axlowdimlem13  28837  hashxpe  32659  ssdifidllem  33268  ssmxidllem  33285  fedgmullem2  33456  gonanegoal  35090  filnetlem4  35993  dihatlat  40934  sn-00id  42088  pellex  42394  nev  43339  ldepspr  47724
  Copyright terms: Public domain W3C validator