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

Theorem necon3abid 2859
 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 2824 . 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 1523   ≠ wne 2823 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 2824 This theorem is referenced by:  necon3bbid  2860  necon2abid  2865  foconst  6164  fndmdif  6361  suppsnop  7354  om00el  7701  oeoa  7722  cardsdom2  8852  mulne0b  10706  crne0  11051  expneg  12908  hashsdom  13208  prprrab  13293  gcdn0gt0  15286  cncongr2  15429  pltval3  17014  mulgnegnn  17598  drngmulne0  18817  lvecvsn0  19157  domnmuln0  19346  mvrf1  19473  connsub  21272  pthaus  21489  xkohaus  21504  bndth  22804  lebnumlem1  22807  dvcobr  23754  dvcnvlem  23784  mdegle0  23882  coemulhi  24055  vieta1lem1  24110  vieta1lem2  24111  aalioulem2  24133  cosne0  24321  atandm3  24650  wilthlem2  24840  issqf  24907  mumullem2  24951  dchrptlem3  25036  lgseisenlem3  25147  brbtwn2  25830  colinearalg  25835  vdn0conngrumgrv2  27174  vdgn1frgrv2  27276  nmlno0lem  27776  nmlnop0iALT  28982  atcvat2i  29374  divnumden2  29692  bnj1542  31053  bnj1253  31211  ptrecube  33539  poimirlem13  33552  ecinn0  34258  llnexchb2  35473  cdlemb3  36211  rencldnfilem  37701  qirropth  37790  binomcxplemfrat  38867  binomcxplemradcnv  38868  odz2prm2pw  41800
 Copyright terms: Public domain W3C validator