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

Theorem necon3abii 3014
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 2969 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abii.1 . 2 (𝐴 = 𝐵𝜑)
31, 2xchbinx 326 1 (𝐴𝐵 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198   = wceq 1601  wne 2968
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 2969
This theorem is referenced by:  necon3bbii  3015  necon3bii  3020  nesym  3024  rabn0  4187  xpimasn  5833  rankxplim3  9041  rankxpsuc  9042  dflt2  12291  gcd0id  15646  lcmfunsnlem2  15759  axlowdimlem13  26303  filnetlem4  32978  dihatlat  37482  pellex  38351  nev  39011  ldepspr  43269
  Copyright terms: Public domain W3C validator