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

Theorem necon3abii 3033
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 2988 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abii.1 . 2 (𝐴 = 𝐵𝜑)
31, 2xchbinx 337 1 (𝐴𝐵 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209   = wceq 1538  wne 2987
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 210  df-ne 2988
This theorem is referenced by:  necon3bbii  3034  necon3bii  3039  nesym  3043  rabn0  4293  xpimasn  6009  rankxplim3  9294  rankxpsuc  9295  dflt2  12529  gcd0id  15857  lcmfunsnlem2  15974  axlowdimlem13  26748  hashxpe  30555  ssmxidllem  31049  fedgmullem2  31114  gonanegoal  32709  filnetlem4  33839  dihatlat  38627  pellex  39771  nev  40466  ldepspr  44877
  Copyright terms: Public domain W3C validator