Theorem necon3abid 2964

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 2929	. 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 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  necon3bbid  2965  necon2abid  2970  prneimg2  4807  prnesn  4812  foconst  6750  fndmdif  6975  suppsnop  8108  om00el  8491  oeoa  8512  cardsdom2  9878  mulne0b  11755  crne0  12115  expneg  13973  hashsdom  14285  prprrab  14377  gcdn0gt0  16426  cncongr2  16576  pltval3  18240  mulgnegnn  18994  domnmuln0  20622  drngmulne0  20675  lvecvsn0  21044  mvrf1  21921  connsub  23334  pthaus  23551  xkohaus  23566  bndth  24882  lebnumlem1  24885  dvcobr  25874  dvcobrOLD  25875  dvcnvlem  25905  mdegle0  26007  coemulhi  26184  vieta1lem1  26243  vieta1lem2  26244  aalioulem2  26266  cosne0  26463  atandm3  26813  wilthlem2  27004  issqf  27071  mumullem2  27115  dchrptlem3  27202  lgseisenlem3  27313  mulsne0bd  28123  brbtwn2  28881  colinearalg  28886  vdn0conngrumgrv2  30171  vdgn1frgrv2  30271  nmlno0lem  30768  nmlnop0iALT  31970  atcvat2i  32362  elq2  32789  divnumden2  32793  domnmuln0rd  33236  lindssn  33338  mxidlirredi  33431  mxidlirred  33432  fedgmullem2  33638  minplyirred  33719  cos9thpiminplylem3  33792  bnj1542  34864  bnj1253  35024  ptrecube  37659  poimirlem13  37672  ecinn0  38380  llnexchb2  39907  cdlemb3  40644  aks6d1c2p2  42151  aks6d1c6lem3  42204  fsuppind  42622  rencldnfilem  42852  qirropth  42940  binomcxplemfrat  44383  binomcxplemradcnv  44384  mod2addne  47394  odz2prm2pw  47593