Theorem necon3abid 2817

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 194   = wceq 1474   ≠ wne 2779

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 195  df-ne 2781

This theorem is referenced by:  necon3bbid  2818  necon2abid  2823  foconst  6024  fndmdif  6214  suppsnop  7173  om00el  7520  oeoa  7541  cardsdom2  8674  mulne0b  10517  crne0  10860  expneg  12685  hashsdom  12983  gcdn0gt0  15023  cncongr2  15166  pltval3  16736  mulgnegnn  17320  drngmulne0  18538  lvecvsn0  18876  domnmuln0  19065  mvrf1  19192  connsub  20976  pthaus  21193  xkohaus  21208  bndth  22496  lebnumlem1  22499  dvcobr  23432  dvcnvlem  23460  mdegle0  23558  coemulhi  23731  vieta1lem1  23786  vieta1lem2  23787  aalioulem2  23809  cosne0  23997  atandm3  24322  wilthlem2  24512  issqf  24579  mumullem2  24623  dchrptlem3  24708  lgseisenlem3  24819  brbtwn2  25503  colinearalg  25508  vdn0frgrav2  26316  vdgn0frgrav2  26317  vdn1frgrav2  26318  vdgn1frgrav2  26319  nmlno0lem  26838  nmlnop0iALT  28044  atcvat2i  28436  divnumden2  28757  bnj1542  29987  bnj1253  30145  ptrecube  32382  poimirlem13  32395  llnexchb2  33976  cdlemb3  34715  rencldnfilem  36205  qirropth  36294  binomcxplemfrat  37375  binomcxplemradcnv  37376  odz2prm2pw  39818  prprrab  40197  vdn0conngrumgrv2  41365  vdgn1frgrv2  41468