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

Theorem necon3abii 3045
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 3000 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abii.1 . 2 (𝐴 = 𝐵𝜑)
31, 2xchbinx 326 1 (𝐴𝐵 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198   = wceq 1656  wne 2999
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 199  df-ne 3000
This theorem is referenced by:  necon3bbii  3046  necon3bii  3051  nesym  3055  rabn0  4187  xpimasn  5820  rankxplim3  9021  rankxpsuc  9022  dflt2  12267  gcd0id  15613  lcmfunsnlem2  15726  axlowdimlem13  26253  filnetlem4  32903  dihatlat  37402  pellex  38236  nev  38896  ldepspr  43102
  Copyright terms: Public domain W3C validator