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

Theorem necon3abid 2932
Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
Hypothesis
Ref Expression
necon3abid.1 (𝜑 → (𝐴 = 𝐵𝜓))
Assertion
Ref Expression
necon3abid (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))

Proof of Theorem necon3abid
StepHypRef Expression
1 df-ne 2897 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32notbid 307 . 2 (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
41, 3syl5bb 272 1 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196   = wceq 1596  wne 2896
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 2897
This theorem is referenced by:  necon3bbid  2933  necon2abid  2938  foconst  6239  fndmdif  6436  suppsnop  7429  om00el  7776  oeoa  7797  cardsdom2  8927  mulne0b  10781  crne0  11126  expneg  12983  hashsdom  13283  prprrab  13368  gcdn0gt0  15362  cncongr2  15505  pltval3  17089  mulgnegnn  17673  drngmulne0  18892  lvecvsn0  19232  domnmuln0  19421  mvrf1  19548  connsub  21347  pthaus  21564  xkohaus  21579  bndth  22879  lebnumlem1  22882  dvcobr  23829  dvcnvlem  23859  mdegle0  23957  coemulhi  24130  vieta1lem1  24185  vieta1lem2  24186  aalioulem2  24208  cosne0  24396  atandm3  24725  wilthlem2  24915  issqf  24982  mumullem2  25026  dchrptlem3  25111  lgseisenlem3  25222  brbtwn2  25905  colinearalg  25910  vdn0conngrumgrv2  27269  vdgn1frgrv2  27371  nmlno0lem  27878  nmlnop0iALT  29084  atcvat2i  29476  divnumden2  29794  bnj1542  31155  bnj1253  31313  ptrecube  33641  poimirlem13  33654  ecinn0  34360  llnexchb2  35575  cdlemb3  36313  rencldnfilem  37803  qirropth  37892  binomcxplemfrat  38969  binomcxplemradcnv  38970  odz2prm2pw  41902
  Copyright terms: Public domain W3C validator