Theorem neneqd 2397

Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
neneqd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Assertion

Ref	Expression
neneqd	⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Proof of Theorem neneqd

Step	Hyp	Ref	Expression
1		neneqd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		df-ne 2377	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylib 122	1 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1373   ≠ wne 2376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-ne 2377

This theorem is referenced by:  neneq  2398  necon2bi  2431  necon2i  2432  pm2.21ddne  2459  nelrdva  2980  neq0r  3475  ifnetruedc  3613  ifnefals  3614  0inp0  4210  pwntru  4243  nndceq0  4666  frecabcl  6485  frecsuclem  6492  nnsucsssuc  6578  phpm  6962  diffisn  6990  en2eqpr  7004  fival  7072  omp1eomlem  7196  difinfsnlem  7201  difinfsn  7202  ctmlemr  7210  nninfisollemne  7233  fodjuomnilemdc  7246  exmidapne  7372  indpi  7455  nqnq0pi  7551  ltxrlt  8138  sup3exmid  9030  elnnz  9382  xrnemnf  9899  xrnepnf  9900  xrlttri3  9919  nltpnft  9936  ngtmnft  9939  xrpnfdc  9964  xrmnfdc  9965  xleaddadd  10009  fzprval  10204  xqltnle  10410  fxnn0nninf  10584  iseqf1olemklt  10643  seq3f1olemqsumkj  10656  expnnval  10687  fihashelne0d  10942  xrmaxrecl  11566  fsumcl2lem  11709  fprodcl2lem  11916  dvdsle  12155  mod2eq1n2dvds  12190  nndvdslegcd  12286  gcdnncl  12288  divgcdnn  12296  sqgcd  12350  eucalgf  12377  eucalginv  12378  lcmeq0  12393  lcmgcdlem  12399  qredeu  12419  rpdvds  12421  cncongr2  12426  divnumden  12518  divdenle  12519  phibndlem  12538  phisum  12563  oddprm  12582  pythagtriplem4  12591  pythagtriplem8  12595  pythagtriplem9  12596  pceq0  12645  4sqlem10  12710  ennnfonelemk  12771  ennnfonelemjn  12773  ennnfonelemp1  12777  ennnfonelemim  12795  mulgnn  13462  rrgnz  14030  aprirr  14045  isxmet2d  14820  dvexp2  15184  dvply1  15237  logbgcd1irraplemexp  15440  perfectlem2  15472  lgsval2lem  15487  lgsval4  15497  lgsdilem  15504  lgsdir  15512  gausslemma2dlem4  15541  lgseisenlem4  15550  lgsquadlem1  15554  lgsquad2  15560  m1lgs  15562  2sqlem8a  15599  2sqlem8  15600  nnsf  15942  peano4nninf  15943  exmidsbthrlem  15961  refeq  15967  trilpolemeq1  15979  dceqnconst  15999