Theorem necon3abid 2980

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

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

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 2944

This theorem is referenced by:  necon3bbid  2981  necon2abid  2986  prnesn  4790  foconst  6703  fndmdif  6919  suppsnop  7994  om00el  8407  oeoa  8428  cardsdom2  9746  mulne0b  11616  crne0  11966  expneg  13790  hashsdom  14096  prprrab  14187  gcdn0gt0  16225  cncongr2  16373  pltval3  18057  mulgnegnn  18714  drngmulne0  20013  lvecvsn0  20371  domnmuln0  20569  mvrf1  21194  connsub  22572  pthaus  22789  xkohaus  22804  bndth  24121  lebnumlem1  24124  dvcobr  25110  dvcnvlem  25140  mdegle0  25242  coemulhi  25415  vieta1lem1  25470  vieta1lem2  25471  aalioulem2  25493  cosne0  25685  atandm3  26028  wilthlem2  26218  issqf  26285  mumullem2  26329  dchrptlem3  26414  lgseisenlem3  26525  brbtwn2  27273  colinearalg  27278  vdn0conngrumgrv2  28560  vdgn1frgrv2  28660  nmlno0lem  29155  nmlnop0iALT  30357  atcvat2i  30749  divnumden2  31132  lindssn  31573  fedgmullem2  31711  bnj1542  32837  bnj1253  32997  ptrecube  35777  poimirlem13  35790  ecinn0  36485  llnexchb2  37883  cdlemb3  38620  fsuppind  40279  rencldnfilem  40642  qirropth  40730  binomcxplemfrat  41969  binomcxplemradcnv  41970  odz2prm2pw  45015