Theorem necon3abid 2962

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 2927	. 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 1540   ≠ wne 2926

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 2927

This theorem is referenced by:  necon3bbid  2963  necon2abid  2968  prneimg2  4822  prnesn  4827  foconst  6790  fndmdif  7017  suppsnop  8160  om00el  8543  oeoa  8564  cardsdom2  9948  mulne0b  11826  crne0  12186  expneg  14041  hashsdom  14353  prprrab  14445  gcdn0gt0  16495  cncongr2  16645  pltval3  18305  mulgnegnn  19023  domnmuln0  20625  drngmulne0  20678  lvecvsn0  21026  mvrf1  21902  connsub  23315  pthaus  23532  xkohaus  23547  bndth  24864  lebnumlem1  24867  dvcobr  25856  dvcobrOLD  25857  dvcnvlem  25887  mdegle0  25989  coemulhi  26166  vieta1lem1  26225  vieta1lem2  26226  aalioulem2  26248  cosne0  26445  atandm3  26795  wilthlem2  26986  issqf  27053  mumullem2  27097  dchrptlem3  27184  lgseisenlem3  27295  mulsne0bd  28096  brbtwn2  28839  colinearalg  28844  vdn0conngrumgrv2  30132  vdgn1frgrv2  30232  nmlno0lem  30729  nmlnop0iALT  31931  atcvat2i  32323  elq2  32743  divnumden2  32747  domnmuln0rd  33232  lindssn  33356  mxidlirredi  33449  mxidlirred  33450  fedgmullem2  33633  minplyirred  33708  cos9thpiminplylem3  33781  bnj1542  34854  bnj1253  35014  ptrecube  37621  poimirlem13  37634  ecinn0  38342  llnexchb2  39870  cdlemb3  40607  aks6d1c2p2  42114  aks6d1c6lem3  42167  fsuppind  42585  rencldnfilem  42815  qirropth  42903  binomcxplemfrat  44347  binomcxplemradcnv  44348  mod2addne  47369  odz2prm2pw  47568