Theorem necon3abid 2996

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

Step	Hyp	Ref	Expression
1		df-ne 2961	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	notbid 321	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
4	1, 3	bitrid 286	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1563   ≠ wne 2960

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 2961

This theorem is referenced by:  necon3bbid  2997  necon2abid  3002  prneimg2  4816  prnesn  4821  foconst  6797  fndmdif  7027  suppsnop  8162  om00el  8549  oeoa  8571  cardsdom2  9962  mulne0b  11843  crne0  12202  expneg  14096  hashsdom  14408  prprrab  14500  gcdn0gt0  16566  cncongr2  16716  pltval3  18383  mulgnegnn  19141  domnmuln0  20785  drngmulne0  20835  lvecvsn0  21202  mvrf1  22095  connsub  23539  pthaus  23756  xkohaus  23771  bndth  25078  lebnumlem1  25081  dvcobr  26066  dvcnvlem  26096  mdegle0  26195  coemulhi  26372  vieta1lem1  26432  vieta1lem2  26433  aalioulem2  26455  cosne0  26652  atandm3  27001  wilthlem2  27191  issqf  27258  mumullem2  27302  dchrptlem3  27388  lgseisenlem3  27499  mulsne0bd  28337  brbtwn2  29164  colinearalg  29169  vdn0conngrumgrv2  30456  vdgn1frgrv2  30556  nmlno0lem  31054  nmlnop0iALT  32256  atcvat2i  32648  elq2  33069  divnumden2  33073  domnmuln0rd  33510  lindssn  33607  mxidlirredi  33671  mxidlirred  33672  deg1prod  33790  fedgmullem2  33937  minplyirred  34018  cos9thpiminplylem3  34091  bnj1542  35162  bnj1253  35322  ptrecube  38131  poimirlem13  38144  ecinn0  38864  llnexchb2  40505  cdlemb3  41242  aks6d1c2p2  42748  aks6d1c6lem3  42801  fsuppind  43184  rencldnfilem  43409  qirropth  43497  binomcxplemfrat  44925  binomcxplemradcnv  44926  mod2addne  47962  odz2prm2pw  48170