Theorem necon3abid 2979

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2942

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 206  df-ne 2943

This theorem is referenced by:  necon3bbid  2980  necon2abid  2985  prnesn  4787  foconst  6687  fndmdif  6901  suppsnop  7965  om00el  8369  oeoa  8390  cardsdom2  9677  mulne0b  11546  crne0  11896  expneg  13718  hashsdom  14024  prprrab  14115  gcdn0gt0  16153  cncongr2  16301  pltval3  17972  mulgnegnn  18629  drngmulne0  19928  lvecvsn0  20286  domnmuln0  20482  mvrf1  21104  connsub  22480  pthaus  22697  xkohaus  22712  bndth  24027  lebnumlem1  24030  dvcobr  25015  dvcnvlem  25045  mdegle0  25147  coemulhi  25320  vieta1lem1  25375  vieta1lem2  25376  aalioulem2  25398  cosne0  25590  atandm3  25933  wilthlem2  26123  issqf  26190  mumullem2  26234  dchrptlem3  26319  lgseisenlem3  26430  brbtwn2  27176  colinearalg  27181  vdn0conngrumgrv2  28461  vdgn1frgrv2  28561  nmlno0lem  29056  nmlnop0iALT  30258  atcvat2i  30650  divnumden2  31034  lindssn  31475  fedgmullem2  31613  bnj1542  32737  bnj1253  32897  ptrecube  35704  poimirlem13  35717  ecinn0  36412  llnexchb2  37810  cdlemb3  38547  fsuppind  40202  rencldnfilem  40558  qirropth  40646  binomcxplemfrat  41858  binomcxplemradcnv  41859  odz2prm2pw  44903