Theorem neneqd 2388

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 2368	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylib 122	1 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1364   ≠ wne 2367

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 2368

This theorem is referenced by:  neneq  2389  necon2bi  2422  necon2i  2423  pm2.21ddne  2450  nelrdva  2971  neq0r  3466  ifnetruedc  3603  ifnefals  3604  0inp0  4200  pwntru  4233  nndceq0  4655  frecabcl  6466  frecsuclem  6473  nnsucsssuc  6559  phpm  6935  diffisn  6963  en2eqpr  6977  fival  7045  omp1eomlem  7169  difinfsnlem  7174  difinfsn  7175  ctmlemr  7183  nninfisollemne  7206  fodjuomnilemdc  7219  exmidapne  7345  indpi  7428  nqnq0pi  7524  ltxrlt  8111  sup3exmid  9003  elnnz  9355  xrnemnf  9871  xrnepnf  9872  xrlttri3  9891  nltpnft  9908  ngtmnft  9911  xrpnfdc  9936  xrmnfdc  9937  xleaddadd  9981  fzprval  10176  xqltnle  10376  fxnn0nninf  10550  iseqf1olemklt  10609  seq3f1olemqsumkj  10622  expnnval  10653  fihashelne0d  10908  xrmaxrecl  11439  fsumcl2lem  11582  fprodcl2lem  11789  dvdsle  12028  mod2eq1n2dvds  12063  nndvdslegcd  12159  gcdnncl  12161  divgcdnn  12169  sqgcd  12223  eucalgf  12250  eucalginv  12251  lcmeq0  12266  lcmgcdlem  12272  qredeu  12292  rpdvds  12294  cncongr2  12299  divnumden  12391  divdenle  12392  phibndlem  12411  phisum  12436  oddprm  12455  pythagtriplem4  12464  pythagtriplem8  12468  pythagtriplem9  12469  pceq0  12518  4sqlem10  12583  ennnfonelemk  12644  ennnfonelemjn  12646  ennnfonelemp1  12650  ennnfonelemim  12668  mulgnn  13334  rrgnz  13902  aprirr  13917  isxmet2d  14692  dvexp2  15056  dvply1  15109  logbgcd1irraplemexp  15312  perfectlem2  15344  lgsval2lem  15359  lgsval4  15369  lgsdilem  15376  lgsdir  15384  gausslemma2dlem4  15413  lgseisenlem4  15422  lgsquadlem1  15426  lgsquad2  15432  m1lgs  15434  2sqlem8a  15471  2sqlem8  15472  nnsf  15760  peano4nninf  15761  exmidsbthrlem  15779  refeq  15785  trilpolemeq1  15797  dceqnconst  15817