Theorem necon3abid 2961

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 2926	. 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 2925

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 2926

This theorem is referenced by:  necon3bbid  2962  necon2abid  2967  prneimg2  4819  prnesn  4824  foconst  6787  fndmdif  7014  suppsnop  8157  om00el  8540  oeoa  8561  cardsdom2  9941  mulne0b  11819  crne0  12179  expneg  14034  hashsdom  14346  prprrab  14438  gcdn0gt0  16488  cncongr2  16638  pltval3  18298  mulgnegnn  19016  domnmuln0  20618  drngmulne0  20671  lvecvsn0  21019  mvrf1  21895  connsub  23308  pthaus  23525  xkohaus  23540  bndth  24857  lebnumlem1  24860  dvcobr  25849  dvcobrOLD  25850  dvcnvlem  25880  mdegle0  25982  coemulhi  26159  vieta1lem1  26218  vieta1lem2  26219  aalioulem2  26241  cosne0  26438  atandm3  26788  wilthlem2  26979  issqf  27046  mumullem2  27090  dchrptlem3  27177  lgseisenlem3  27288  mulsne0bd  28089  brbtwn2  28832  colinearalg  28837  vdn0conngrumgrv2  30125  vdgn1frgrv2  30225  nmlno0lem  30722  nmlnop0iALT  31924  atcvat2i  32316  elq2  32736  divnumden2  32740  domnmuln0rd  33225  lindssn  33349  mxidlirredi  33442  mxidlirred  33443  fedgmullem2  33626  minplyirred  33701  cos9thpiminplylem3  33774  bnj1542  34847  bnj1253  35007  ptrecube  37614  poimirlem13  37627  ecinn0  38335  llnexchb2  39863  cdlemb3  40600  aks6d1c2p2  42107  aks6d1c6lem3  42160  fsuppind  42578  rencldnfilem  42808  qirropth  42896  binomcxplemfrat  44340  binomcxplemradcnv  44341  mod2addne  47365  odz2prm2pw  47564