Theorem necon3abid 2969

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  necon3bbid  2970  necon2abid  2975  prneimg2  4799  prnesn  4804  foconst  6761  fndmdif  6988  suppsnop  8121  om00el  8504  oeoa  8526  cardsdom2  9903  mulne0b  11782  crne0  12143  expneg  14022  hashsdom  14334  prprrab  14426  gcdn0gt0  16478  cncongr2  16628  pltval3  18294  mulgnegnn  19051  domnmuln0  20677  drngmulne0  20730  lvecvsn0  21099  mvrf1  21974  connsub  23396  pthaus  23613  xkohaus  23628  bndth  24935  lebnumlem1  24938  dvcobr  25923  dvcnvlem  25953  mdegle0  26052  coemulhi  26229  vieta1lem1  26287  vieta1lem2  26288  aalioulem2  26310  cosne0  26506  atandm3  26855  wilthlem2  27046  issqf  27113  mumullem2  27157  dchrptlem3  27243  lgseisenlem3  27354  mulsne0bd  28192  brbtwn2  28988  colinearalg  28993  vdn0conngrumgrv2  30281  vdgn1frgrv2  30381  nmlno0lem  30879  nmlnop0iALT  32081  atcvat2i  32473  elq2  32900  divnumden2  32904  domnmuln0rd  33350  lindssn  33453  mxidlirredi  33546  mxidlirred  33547  deg1prod  33658  fedgmullem2  33790  minplyirred  33871  cos9thpiminplylem3  33944  bnj1542  35015  bnj1253  35175  ptrecube  37955  poimirlem13  37968  ecinn0  38688  llnexchb2  40329  cdlemb3  41066  aks6d1c2p2  42572  aks6d1c6lem3  42625  fsuppind  43037  rencldnfilem  43266  qirropth  43354  binomcxplemfrat  44796  binomcxplemradcnv  44797  mod2addne  47830  odz2prm2pw  48038