Theorem necon3abid 2967

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 2932	. 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 1539   ≠ wne 2931

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 2932

This theorem is referenced by:  necon3bbid  2968  necon2abid  2973  prneimg2  4835  prnesn  4840  foconst  6815  fndmdif  7042  suppsnop  8185  om00el  8596  oeoa  8617  cardsdom2  10010  mulne0b  11886  crne0  12241  expneg  14092  hashsdom  14402  prprrab  14494  gcdn0gt0  16537  cncongr2  16687  pltval3  18353  mulgnegnn  19071  domnmuln0  20677  drngmulne0  20730  lvecvsn0  21079  mvrf1  21960  connsub  23375  pthaus  23592  xkohaus  23607  bndth  24926  lebnumlem1  24929  dvcobr  25919  dvcobrOLD  25920  dvcnvlem  25950  mdegle0  26052  coemulhi  26229  vieta1lem1  26288  vieta1lem2  26289  aalioulem2  26311  cosne0  26507  atandm3  26857  wilthlem2  27048  issqf  27115  mumullem2  27159  dchrptlem3  27246  lgseisenlem3  27357  mulsne0bd  28148  brbtwn2  28850  colinearalg  28855  vdn0conngrumgrv2  30143  vdgn1frgrv2  30243  nmlno0lem  30740  nmlnop0iALT  31942  atcvat2i  32334  divnumden2  32757  domnmuln0rd  33217  lindssn  33341  mxidlirredi  33434  mxidlirred  33435  fedgmullem2  33616  minplyirred  33691  bnj1542  34830  bnj1253  34990  ptrecube  37586  poimirlem13  37599  ecinn0  38313  llnexchb2  39830  cdlemb3  40567  aks6d1c2p2  42079  aks6d1c6lem3  42132  fsuppind  42563  rencldnfilem  42794  qirropth  42882  binomcxplemfrat  44327  binomcxplemradcnv  44328  odz2prm2pw  47508