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

Theorem necon3abii 2839
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 2794 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abii.1 . 2 (𝐴 = 𝐵𝜑)
31, 2xchbinx 324 1 (𝐴𝐵 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1482  wne 2793
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 2794
This theorem is referenced by:  necon3bbii  2840  necon3bii  2845  nesym  2849  n0fOLD  3926  rabn0  3956  xpimasn  5577  rankxplim3  8741  rankxpsuc  8742  dflt2  11978  gcd0id  15234  lcmfunsnlem2  15347  axlowdimlem13  25828  filnetlem4  32360  dihatlat  36449  pellex  37225  nev  37888  ldepspr  42033
  Copyright terms: Public domain W3C validator