Theorem necon3abid 2992

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 2957	. 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 2956

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 2957

This theorem is used by:  necon3bbid  2993  necon2abid  2998  prneimg2  4815  prnesn  4820  foconst  6803  fndmdif  7033  suppsnop  8179  tz7.48lem  8434  om00el  8568  oeoa  8590  cardsdom2  10050  mulne0b  11938  crne0  12294  expneg  14192  hashsdom  14505  prprrab  14598  gcdn0gt0  16670  cncongr2  16823  pltval3  18491  mulgnegnn  19274  domnmuln0  20941  drngmulne0  20999  lvecvsn0  21367  mvrf1  22273  connsub  23719  pthaus  23937  xkohaus  23952  bndth  25259  lebnumlem1  25262  dvcobr  26246  dvcnvlem  26276  mdegle0  26375  coemulhi  26553  vieta1lem1  26615  vieta1lem2  26616  aalioulem2  26642  cosne0  26839  atandm3  27188  wilthlem2  27378  issqf  27445  mumullem2  27489  dchrptlem3  27575  lgseisenlem3  27686  mulsne0bd  28554  brbtwn2  29465  colinearalg  29470  vdn0conngrumgrv2  30779  vdgn1frgrv2  30879  nmlno0lem  31377  nmlnop0iALT  32579  atcvat2i  32971  elq2  33385  divnumden2  33389  domnmuln0rd  33820  lindssn  33915  mxidlirredi  33978  mxidlirred  33979  deg1prod  34097  fedgmullem2  34244  minplyirred  34325  cos9thpiminplylem3  34398  bnj1542  35470  bnj1253  35630  ptrecube  38506  poimirlem13  38519  ecinn0  39253  llnexchb2  40894  cdlemb3  41631  aks6d1c2p2  43137  aks6d1c6lem3  43190  fsuppind  43580  rencldnfilem  43780  qirropth  43868  binomcxplemfrat  45294  binomcxplemradcnv  45295  mod2addne  48384  odz2prm2pw  48592