Theorem necon3abid 2987

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 2952	. 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 2951

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 2952

This theorem is referenced by:  necon3bbid  2988  necon2abid  2993  prnesn  4747  foconst  6589  fndmdif  6803  suppsnop  7852  om00el  8212  oeoa  8233  cardsdom2  9450  mulne0b  11319  crne0  11667  expneg  13487  hashsdom  13792  prprrab  13883  gcdn0gt0  15917  cncongr2  16064  pltval3  17643  mulgnegnn  18305  drngmulne0  19592  lvecvsn0  19949  domnmuln0  20139  mvrf1  20753  connsub  22121  pthaus  22338  xkohaus  22353  bndth  23659  lebnumlem1  23662  dvcobr  24645  dvcnvlem  24675  mdegle0  24777  coemulhi  24950  vieta1lem1  25005  vieta1lem2  25006  aalioulem2  25028  cosne0  25220  atandm3  25563  wilthlem2  25753  issqf  25820  mumullem2  25864  dchrptlem3  25949  lgseisenlem3  26060  brbtwn2  26798  colinearalg  26803  vdn0conngrumgrv2  28080  vdgn1frgrv2  28180  nmlno0lem  28675  nmlnop0iALT  29877  atcvat2i  30269  divnumden2  30656  lindssn  31094  fedgmullem2  31232  bnj1542  32357  bnj1253  32517  ptrecube  35337  poimirlem13  35350  ecinn0  36047  llnexchb2  37445  cdlemb3  38182  fsuppind  39784  rencldnfilem  40134  qirropth  40222  binomcxplemfrat  41428  binomcxplemradcnv  41429  odz2prm2pw  44448