Theorem necon3abid 2975

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 2939	. 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 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  necon3bbid  2976  necon2abid  2981  prneimg2  4860  prnesn  4865  foconst  6836  fndmdif  7062  suppsnop  8202  om00el  8613  oeoa  8634  cardsdom2  10026  mulne0b  11902  crne0  12257  expneg  14107  hashsdom  14417  prprrab  14509  gcdn0gt0  16552  cncongr2  16702  pltval3  18397  mulgnegnn  19115  domnmuln0  20726  drngmulne0  20779  lvecvsn0  21129  mvrf1  22024  connsub  23445  pthaus  23662  xkohaus  23677  bndth  25004  lebnumlem1  25007  dvcobr  25998  dvcobrOLD  25999  dvcnvlem  26029  mdegle0  26131  coemulhi  26308  vieta1lem1  26367  vieta1lem2  26368  aalioulem2  26390  cosne0  26586  atandm3  26936  wilthlem2  27127  issqf  27194  mumullem2  27238  dchrptlem3  27325  lgseisenlem3  27436  mulsne0bd  28227  brbtwn2  28935  colinearalg  28940  vdn0conngrumgrv2  30225  vdgn1frgrv2  30325  nmlno0lem  30822  nmlnop0iALT  32024  atcvat2i  32416  divnumden2  32822  domnmuln0rd  33261  lindssn  33386  mxidlirredi  33479  mxidlirred  33480  fedgmullem2  33658  minplyirred  33719  bnj1542  34850  bnj1253  35010  ptrecube  37607  poimirlem13  37620  ecinn0  38335  llnexchb2  39852  cdlemb3  40589  aks6d1c2p2  42101  aks6d1c6lem3  42154  fsuppind  42577  rencldnfilem  42808  qirropth  42896  binomcxplemfrat  44347  binomcxplemradcnv  44348  odz2prm2pw  47488