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

Theorem necon3abii 2836
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 2791 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abii.1 . 2 (𝐴 = 𝐵𝜑)
31, 2xchbinx 324 1 (𝐴𝐵 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1480  wne 2790
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 197  df-ne 2791
This theorem is referenced by:  necon3bbii  2837  necon3bii  2842  nesym  2846  n0fOLD  3909  rabn0  3937  xpimasn  5543  rankxplim3  8696  rankxpsuc  8697  dflt2  11933  gcd0id  15175  lcmfunsnlem2  15288  axlowdimlem13  25751  filnetlem4  32053  dihatlat  36138  pellex  36914  nev  37578  ldepspr  41576
  Copyright terms: Public domain W3C validator