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

Theorem necon3abii 3062
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 3017 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abii.1 . 2 (𝐴 = 𝐵𝜑)
31, 2xchbinx 335 1 (𝐴𝐵 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon3bbii  3063  necon3bii  3068  nesym  3072  rabn0  4338  xpimasn  6036  rankxplim3  9299  rankxpsuc  9300  dflt2  12531  gcd0id  15857  lcmfunsnlem2  15974  axlowdimlem13  26668  hashxpe  30456  fedgmullem2  30926  gonanegoal  32497  filnetlem4  33627  dihatlat  38352  pellex  39312  nev  39995  ldepspr  44426
  Copyright terms: Public domain W3C validator