Theorem necon3abid 2992

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necon3bbid  2993  necon2abid  2998  prneimg2  4812  prnesn  4817  foconst  6789  fndmdif  7019  suppsnop  8153  om00el  8540  oeoa  8562  cardsdom2  9943  mulne0b  11825  crne0  12185  expneg  14079  hashsdom  14391  prprrab  14483  gcdn0gt0  16535  cncongr2  16685  pltval3  18352  mulgnegnn  19109  domnmuln0  20738  drngmulne0  20791  lvecvsn0  21159  mvrf1  22017  connsub  23461  pthaus  23678  xkohaus  23693  bndth  25000  lebnumlem1  25003  dvcobr  25988  dvcnvlem  26018  mdegle0  26117  coemulhi  26294  vieta1lem1  26351  vieta1lem2  26352  aalioulem2  26374  cosne0  26571  atandm3  26920  wilthlem2  27110  issqf  27177  mumullem2  27221  dchrptlem3  27307  lgseisenlem3  27418  mulsne0bd  28256  brbtwn2  29052  colinearalg  29057  vdn0conngrumgrv2  30344  vdgn1frgrv2  30444  nmlno0lem  30942  nmlnop0iALT  32144  atcvat2i  32536  elq2  32964  divnumden2  32968  domnmuln0rd  33419  lindssn  33525  mxidlirredi  33620  mxidlirred  33621  deg1prod  33740  fedgmullem2  33888  minplyirred  33969  cos9thpiminplylem3  34042  bnj1542  35116  bnj1253  35276  ptrecube  38083  poimirlem13  38096  ecinn0  38816  llnexchb2  40457  cdlemb3  41194  aks6d1c2p2  42700  aks6d1c6lem3  42753  fsuppind  43136  rencldnfilem  43361  qirropth  43449  binomcxplemfrat  44891  binomcxplemradcnv  44892  mod2addne  47928  odz2prm2pw  48136