Theorem necon3abid 2818

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon3bbid  2819  necon2abid  2824  foconst  6039  fndmdif  6229  suppsnop  7196  om00el  7543  oeoa  7564  cardsdom2  8697  mulne0b  10547  crne0  10890  expneg  12730  hashsdom  13031  prprrab  13112  gcdn0gt0  15077  cncongr2  15220  pltval3  16790  mulgnegnn  17374  drngmulne0  18592  lvecvsn0  18930  domnmuln0  19119  mvrf1  19246  connsub  21034  pthaus  21251  xkohaus  21266  bndth  22565  lebnumlem1  22568  dvcobr  23515  dvcnvlem  23543  mdegle0  23641  coemulhi  23814  vieta1lem1  23869  vieta1lem2  23870  aalioulem2  23892  cosne0  24080  atandm3  24405  wilthlem2  24595  issqf  24662  mumullem2  24706  dchrptlem3  24791  lgseisenlem3  24902  brbtwn2  25585  colinearalg  25590  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdn1frgrav2  26552  vdgn1frgrav2  26553  nmlno0lem  27032  nmlnop0iALT  28238  atcvat2i  28630  divnumden2  28951  bnj1542  30181  bnj1253  30339  ptrecube  32579  poimirlem13  32592  llnexchb2  34173  cdlemb3  34912  rencldnfilem  36402  qirropth  36491  binomcxplemfrat  37572  binomcxplemradcnv  37573  odz2prm2pw  40013  vdn0conngrumgrv2  41363  vdgn1frgrv2  41466