Theorem necon3abid 3023

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

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

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 2988

This theorem is referenced by:  necon3bbid  3024  necon2abid  3029  prnesn  4750  foconst  6578  fndmdif  6789  suppsnop  7827  om00el  8185  oeoa  8206  cardsdom2  9401  mulne0b  11270  crne0  11618  expneg  13433  hashsdom  13738  prprrab  13827  gcdn0gt0  15856  cncongr2  16002  pltval3  17569  mulgnegnn  18230  drngmulne0  19517  lvecvsn0  19874  domnmuln0  20064  mvrf1  20663  connsub  22026  pthaus  22243  xkohaus  22258  bndth  23563  lebnumlem1  23566  dvcobr  24549  dvcnvlem  24579  mdegle0  24678  coemulhi  24851  vieta1lem1  24906  vieta1lem2  24907  aalioulem2  24929  cosne0  25121  atandm3  25464  wilthlem2  25654  issqf  25721  mumullem2  25765  dchrptlem3  25850  lgseisenlem3  25961  brbtwn2  26699  colinearalg  26704  vdn0conngrumgrv2  27981  vdgn1frgrv2  28081  nmlno0lem  28576  nmlnop0iALT  29778  atcvat2i  30170  divnumden2  30560  lindssn  30993  fedgmullem2  31114  bnj1542  32239  bnj1253  32399  ptrecube  35057  poimirlem13  35070  ecinn0  35767  llnexchb2  37165  cdlemb3  37902  fsuppind  39456  rencldnfilem  39761  qirropth  39849  binomcxplemfrat  41055  binomcxplemradcnv  41056  odz2prm2pw  44080