Theorem neneqd 2368

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1353   ≠ wne 2347

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 2348

This theorem is referenced by:  neneq  2369  necon2bi  2402  necon2i  2403  pm2.21ddne  2430  nelrdva  2945  neq0r  3438  0inp0  4167  pwntru  4200  nndceq0  4618  frecabcl  6400  frecsuclem  6407  nnsucsssuc  6493  phpm  6865  diffisn  6893  en2eqpr  6907  fival  6969  omp1eomlem  7093  difinfsnlem  7098  difinfsn  7099  ctmlemr  7107  nninfisollemne  7129  fodjuomnilemdc  7142  exmidapne  7259  indpi  7341  nqnq0pi  7437  ltxrlt  8023  sup3exmid  8914  elnnz  9263  xrnemnf  9777  xrnepnf  9778  xrlttri3  9797  nltpnft  9814  ngtmnft  9817  xrpnfdc  9842  xrmnfdc  9843  xleaddadd  9887  fzprval  10082  fxnn0nninf  10438  iseqf1olemklt  10485  seq3f1olemqsumkj  10498  expnnval  10523  fihashelne0d  10777  xrmaxrecl  11263  fsumcl2lem  11406  fprodcl2lem  11613  dvdsle  11850  mod2eq1n2dvds  11884  nndvdslegcd  11966  gcdnncl  11968  divgcdnn  11976  sqgcd  12030  eucalgf  12055  eucalginv  12056  lcmeq0  12071  lcmgcdlem  12077  qredeu  12097  rpdvds  12099  cncongr2  12104  divnumden  12196  divdenle  12197  phibndlem  12216  phisum  12240  oddprm  12259  pythagtriplem4  12268  pythagtriplem8  12272  pythagtriplem9  12273  pceq0  12321  4sqlem10  12385  ennnfonelemk  12401  ennnfonelemjn  12403  ennnfonelemp1  12407  ennnfonelemim  12425  mulgnn  12989  aprirr  13373  isxmet2d  13851  dvexp2  14179  logbgcd1irraplemexp  14389  lgsval2lem  14414  lgsval4  14424  lgsdilem  14431  lgsdir  14439  m1lgs  14455  2sqlem8a  14472  2sqlem8  14473  nnsf  14757  peano4nninf  14758  exmidsbthrlem  14773  refeq  14779  trilpolemeq1  14791  dceqnconst  14810