Theorem necon3abid 2993

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2958

This theorem is used by:  necon3bbid  2994  necon2abid  2999  prneimg2  4818  prnesn  4823  foconst  6808  fndmdif  7038  suppsnop  8180  om00el  8567  oeoa  8589  cardsdom2  9997  mulne0b  11883  crne0  12239  expneg  14137  hashsdom  14449  prprrab  14542  gcdn0gt0  16614  cncongr2  16764  pltval3  18431  mulgnegnn  19213  domnmuln0  20877  drngmulne0  20934  lvecvsn0  21302  mvrf1  22206  connsub  23652  pthaus  23870  xkohaus  23885  bndth  25192  lebnumlem1  25195  dvcobr  26180  dvcnvlem  26210  mdegle0  26309  coemulhi  26487  vieta1lem1  26549  vieta1lem2  26550  aalioulem2  26576  cosne0  26774  atandm3  27123  wilthlem2  27313  issqf  27380  mumullem2  27424  dchrptlem3  27510  lgseisenlem3  27621  mulsne0bd  28459  brbtwn2  29370  colinearalg  29375  vdn0conngrumgrv2  30684  vdgn1frgrv2  30784  nmlno0lem  31282  nmlnop0iALT  32484  atcvat2i  32876  elq2  33290  divnumden2  33294  domnmuln0rd  33725  lindssn  33819  mxidlirredi  33882  mxidlirred  33883  deg1prod  34001  fedgmullem2  34148  minplyirred  34229  cos9thpiminplylem3  34302  bnj1542  35374  bnj1253  35534  ptrecube  38377  poimirlem13  38390  ecinn0  39109  llnexchb2  40750  cdlemb3  41487  aks6d1c2p2  42993  aks6d1c6lem3  43046  fsuppind  43444  rencldnfilem  43669  qirropth  43757  binomcxplemfrat  45183  binomcxplemradcnv  45184  mod2addne  48266  odz2prm2pw  48474