Theorem necon3abid 2976

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

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

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 2940

This theorem is referenced by:  necon3bbid  2977  necon2abid  2982  prnesn  4860  foconst  6820  fndmdif  7043  suppsnop  8167  om00el  8580  oeoa  8601  cardsdom2  9987  mulne0b  11860  crne0  12210  expneg  14040  hashsdom  14346  prprrab  14439  gcdn0gt0  16464  cncongr2  16610  pltval3  18297  mulgnegnn  19001  drngmulne0  20531  lvecvsn0  20868  domnmuln0  21115  mvrf1  21765  connsub  23146  pthaus  23363  xkohaus  23378  bndth  24705  lebnumlem1  24708  dvcobr  25698  dvcobrOLD  25699  dvcnvlem  25729  mdegle0  25831  coemulhi  26004  vieta1lem1  26060  vieta1lem2  26061  aalioulem2  26083  cosne0  26275  atandm3  26620  wilthlem2  26810  issqf  26877  mumullem2  26921  dchrptlem3  27006  lgseisenlem3  27117  brbtwn2  28431  colinearalg  28436  vdn0conngrumgrv2  29717  vdgn1frgrv2  29817  nmlno0lem  30314  nmlnop0iALT  31516  atcvat2i  31908  divnumden2  32292  lindssn  32769  mxidlirredi  32862  mxidlirred  32863  fedgmullem2  33004  minplyirred  33060  bnj1542  34167  bnj1253  34327  ptrecube  36792  poimirlem13  36805  ecinn0  37526  llnexchb2  39044  cdlemb3  39781  aks6d1c2p2  41264  fsuppind  41465  rencldnfilem  41861  qirropth  41949  binomcxplemfrat  43413  binomcxplemradcnv  43414  odz2prm2pw  46530