Theorem necon3abid 2968

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 206   = wceq 1542   ≠ 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 207  df-ne 2933

This theorem is referenced by:  necon3bbid  2969  necon2abid  2974  prneimg2  4798  prnesn  4803  foconst  6767  fndmdif  6994  suppsnop  8128  om00el  8511  oeoa  8533  cardsdom2  9912  mulne0b  11791  crne0  12152  expneg  14031  hashsdom  14343  prprrab  14435  gcdn0gt0  16487  cncongr2  16637  pltval3  18303  mulgnegnn  19060  domnmuln0  20686  drngmulne0  20739  lvecvsn0  21107  mvrf1  21964  connsub  23386  pthaus  23603  xkohaus  23618  bndth  24925  lebnumlem1  24928  dvcobr  25913  dvcnvlem  25943  mdegle0  26042  coemulhi  26219  vieta1lem1  26276  vieta1lem2  26277  aalioulem2  26299  cosne0  26493  atandm3  26842  wilthlem2  27032  issqf  27099  mumullem2  27143  dchrptlem3  27229  lgseisenlem3  27340  mulsne0bd  28178  brbtwn2  28974  colinearalg  28979  vdn0conngrumgrv2  30266  vdgn1frgrv2  30366  nmlno0lem  30864  nmlnop0iALT  32066  atcvat2i  32458  elq2  32885  divnumden2  32889  domnmuln0rd  33335  lindssn  33438  mxidlirredi  33531  mxidlirred  33532  deg1prod  33643  fedgmullem2  33774  minplyirred  33855  cos9thpiminplylem3  33928  bnj1542  34999  bnj1253  35159  ptrecube  37941  poimirlem13  37954  ecinn0  38674  llnexchb2  40315  cdlemb3  41052  aks6d1c2p2  42558  aks6d1c6lem3  42611  fsuppind  43023  rencldnfilem  43248  qirropth  43336  binomcxplemfrat  44778  binomcxplemradcnv  44779  mod2addne  47818  odz2prm2pw  48026