Theorem necon3abid 2969

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 2933	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	notbid 318	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
4	1, 3	bitrid 283	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

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

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 2933

This theorem is referenced by:  necon3bbid  2970  necon2abid  2975  prnesn  4853  foconst  6811  fndmdif  7034  suppsnop  8158  om00el  8572  oeoa  8593  cardsdom2  9980  mulne0b  11853  crne0  12203  expneg  14033  hashsdom  14339  prprrab  14432  gcdn0gt0  16458  cncongr2  16604  pltval3  18296  mulgnegnn  19003  drngmulne0  20609  lvecvsn0  20952  domnmuln0  21200  mvrf1  21857  connsub  23249  pthaus  23466  xkohaus  23481  bndth  24808  lebnumlem1  24811  dvcobr  25801  dvcobrOLD  25802  dvcnvlem  25832  mdegle0  25937  coemulhi  26110  vieta1lem1  26166  vieta1lem2  26167  aalioulem2  26189  cosne0  26382  atandm3  26729  wilthlem2  26920  issqf  26987  mumullem2  27031  dchrptlem3  27118  lgseisenlem3  27229  mulsne0bd  28005  brbtwn2  28635  colinearalg  28640  vdn0conngrumgrv2  29921  vdgn1frgrv2  30021  nmlno0lem  30518  nmlnop0iALT  31720  atcvat2i  32112  divnumden2  32494  lindssn  32966  mxidlirredi  33059  mxidlirred  33060  fedgmullem2  33197  minplyirred  33253  bnj1542  34359  bnj1253  34519  ptrecube  36982  poimirlem13  36995  ecinn0  37716  llnexchb2  39234  cdlemb3  39971  aks6d1c2p2  41454  fsuppind  41655  rencldnfilem  42072  qirropth  42160  binomcxplemfrat  43624  binomcxplemradcnv  43625  odz2prm2pw  46741