Theorem necon3abid 2975

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 2939	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	notbid 317	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
4	1, 3	bitrid 282	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2938

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 206  df-ne 2939

This theorem is referenced by:  necon3bbid  2976  necon2abid  2981  prnesn  4859  foconst  6819  fndmdif  7042  suppsnop  8165  om00el  8578  oeoa  8599  cardsdom2  9985  mulne0b  11859  crne0  12209  expneg  14039  hashsdom  14345  prprrab  14438  gcdn0gt0  16463  cncongr2  16609  pltval3  18296  mulgnegnn  19000  drngmulne0  20530  lvecvsn0  20867  domnmuln0  21114  mvrf1  21764  connsub  23145  pthaus  23362  xkohaus  23377  bndth  24704  lebnumlem1  24707  dvcobr  25697  dvcobrOLD  25698  dvcnvlem  25728  mdegle0  25830  coemulhi  26003  vieta1lem1  26059  vieta1lem2  26060  aalioulem2  26082  cosne0  26274  atandm3  26619  wilthlem2  26809  issqf  26876  mumullem2  26920  dchrptlem3  27005  lgseisenlem3  27116  brbtwn2  28430  colinearalg  28435  vdn0conngrumgrv2  29716  vdgn1frgrv2  29816  nmlno0lem  30313  nmlnop0iALT  31515  atcvat2i  31907  divnumden2  32291  lindssn  32768  mxidlirredi  32861  mxidlirred  32862  fedgmullem2  33003  minplyirred  33059  bnj1542  34166  bnj1253  34326  ptrecube  36791  poimirlem13  36804  ecinn0  37525  llnexchb2  39043  cdlemb3  39780  aks6d1c2p2  41263  fsuppind  41464  rencldnfilem  41860  qirropth  41948  binomcxplemfrat  43412  binomcxplemradcnv  43413  odz2prm2pw  46529