Theorem necon3abid 2994

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  necon3bbid  2995  necon2abid  3000  prneimg2  4821  prnesn  4826  foconst  6809  fndmdif  7039  suppsnop  8175  om00el  8562  oeoa  8584  cardsdom2  9975  mulne0b  11856  crne0  12212  expneg  14107  hashsdom  14419  prprrab  14512  gcdn0gt0  16577  cncongr2  16727  pltval3  18394  mulgnegnn  19151  domnmuln0  20795  drngmulne0  20847  lvecvsn0  21214  mvrf1  22116  connsub  23559  pthaus  23776  xkohaus  23791  bndth  25098  lebnumlem1  25101  dvcobr  26086  dvcnvlem  26116  mdegle0  26215  coemulhi  26392  vieta1lem1  26452  vieta1lem2  26453  aalioulem2  26475  cosne0  26672  atandm3  27021  wilthlem2  27211  issqf  27278  mumullem2  27322  dchrptlem3  27408  lgseisenlem3  27519  mulsne0bd  28357  brbtwn2  29233  colinearalg  29238  vdn0conngrumgrv2  30525  vdgn1frgrv2  30625  nmlno0lem  31123  nmlnop0iALT  32325  atcvat2i  32717  elq2  33134  divnumden2  33138  domnmuln0rd  33575  lindssn  33669  mxidlirredi  33732  mxidlirred  33733  deg1prod  33851  fedgmullem2  33998  minplyirred  34079  cos9thpiminplylem3  34152  bnj1542  35223  bnj1253  35383  ptrecube  38249  poimirlem13  38262  ecinn0  38980  llnexchb2  40621  cdlemb3  41358  aks6d1c2p2  42864  aks6d1c6lem3  42917  fsuppind  43302  rencldnfilem  43527  qirropth  43615  binomcxplemfrat  45041  binomcxplemradcnv  45042  mod2addne  48084  odz2prm2pw  48292