Theorem neneqd 2385

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

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

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 2365

This theorem is referenced by:  neneq  2386  necon2bi  2419  necon2i  2420  pm2.21ddne  2447  nelrdva  2968  neq0r  3462  ifnetruedc  3599  ifnefals  3600  0inp0  4196  pwntru  4229  nndceq0  4651  frecabcl  6454  frecsuclem  6461  nnsucsssuc  6547  phpm  6923  diffisn  6951  en2eqpr  6965  fival  7031  omp1eomlem  7155  difinfsnlem  7160  difinfsn  7161  ctmlemr  7169  nninfisollemne  7192  fodjuomnilemdc  7205  exmidapne  7322  indpi  7404  nqnq0pi  7500  ltxrlt  8087  sup3exmid  8978  elnnz  9330  xrnemnf  9846  xrnepnf  9847  xrlttri3  9866  nltpnft  9883  ngtmnft  9886  xrpnfdc  9911  xrmnfdc  9912  xleaddadd  9956  fzprval  10151  xqltnle  10339  fxnn0nninf  10513  iseqf1olemklt  10572  seq3f1olemqsumkj  10585  expnnval  10616  fihashelne0d  10871  xrmaxrecl  11401  fsumcl2lem  11544  fprodcl2lem  11751  dvdsle  11989  mod2eq1n2dvds  12023  nndvdslegcd  12105  gcdnncl  12107  divgcdnn  12115  sqgcd  12169  eucalgf  12196  eucalginv  12197  lcmeq0  12212  lcmgcdlem  12218  qredeu  12238  rpdvds  12240  cncongr2  12245  divnumden  12337  divdenle  12338  phibndlem  12357  phisum  12381  oddprm  12400  pythagtriplem4  12409  pythagtriplem8  12413  pythagtriplem9  12414  pceq0  12463  4sqlem10  12528  ennnfonelemk  12560  ennnfonelemjn  12562  ennnfonelemp1  12566  ennnfonelemim  12584  mulgnn  13199  rrgnz  13767  aprirr  13782  isxmet2d  14527  dvexp2  14891  dvply1  14943  logbgcd1irraplemexp  15141  lgsval2lem  15167  lgsval4  15177  lgsdilem  15184  lgsdir  15192  gausslemma2dlem4  15221  lgseisenlem4  15230  lgsquadlem1  15234  lgsquad2  15240  m1lgs  15242  2sqlem8a  15279  2sqlem8  15280  nnsf  15565  peano4nninf  15566  exmidsbthrlem  15582  refeq  15588  trilpolemeq1  15600  dceqnconst  15620