Theorem necon3abid 3005

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 2970	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	notbid 310	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
4	1, 3	syl5bb 275	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   = wceq 1653   ≠ wne 2969

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 199  df-ne 2970

This theorem is referenced by:  necon3bbid  3006  necon2abid  3011  prnesn  4577  foconst  6342  fndmdif  6545  suppsnop  7544  om00el  7894  oeoa  7915  cardsdom2  9098  mulne0b  10958  crne0  11303  expneg  13118  hashsdom  13416  prprrab  13500  gcdn0gt0  15571  cncongr2  15713  pltval3  17279  mulgnegnn  17864  drngmulne0  19084  lvecvsn0  19427  domnmuln0  19618  mvrf1  19745  connsub  21550  pthaus  21767  xkohaus  21782  bndth  23082  lebnumlem1  23085  dvcobr  24047  dvcnvlem  24077  mdegle0  24175  coemulhi  24348  vieta1lem1  24403  vieta1lem2  24404  aalioulem2  24426  cosne0  24615  atandm3  24954  wilthlem2  25144  issqf  25211  mumullem2  25255  dchrptlem3  25340  lgseisenlem3  25451  brbtwn2  26134  colinearalg  26139  vdn0conngrumgrv2  27532  vdgn1frgrv2  27637  nmlno0lem  28165  nmlnop0iALT  29371  atcvat2i  29763  divnumden2  30074  bnj1542  31436  bnj1253  31594  ptrecube  33890  poimirlem13  33903  ecinn0  34604  llnexchb2  35882  cdlemb3  36619  rencldnfilem  38158  qirropth  38246  binomcxplemfrat  39320  binomcxplemradcnv  39321  odz2prm2pw  42245