Theorem neneqd 2441

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  neneq  2442  necon2bi  2475  necon2i  2476  pm2.21ddne  2503  nelrdva  3033  neq0r  3536  ifnetruedc  3684  ifnefals  3685  0inp0  4305  pwntru  4338  nndceq0  4767  fczsupp0  6503  frecabcl  6675  frecsuclem  6682  nnsucsssuc  6770  phpm  7173  diffisn  7203  en2eqpr  7220  fival  7309  omp1eomlem  7440  difinfsnlem  7445  difinfsn  7446  ctmlemr  7454  nninfisollemne  7477  fodjuomnilemdc  7490  exmidapne  7632  indpi  7715  nqnq0pi  7811  ltxrlt  8397  sup3exmid  9295  elnnz  9663  xrnemnf  10195  xrnepnf  10196  xrlttri3  10215  nltpnft  10232  ngtmnft  10235  xrpnfdc  10260  xrmnfdc  10261  xleaddadd  10305  fzprval  10505  fzodisjsn  10607  xqltnle  10718  fxnn0nninf  10896  iseqf1olemklt  10955  seq3f1olemqsumkj  10968  expnnval  10999  fihashelne0d  11257  xrmaxrecl  12045  fsumcl2lem  12189  fprodcl2lem  12396  dvdsle  12635  mod2eq1n2dvds  12670  nndvdslegcd  12766  gcdnncl  12768  divgcdnn  12776  sqgcd  12830  eucalgf  12857  eucalginv  12858  lcmeq0  12873  lcmgcdlem  12879  qredeu  12899  rpdvds  12901  cncongr2  12906  divnumden  13000  divdenle  13001  phibndlem  13022  phisum  13047  oddprm  13066  pythagtriplem4  13075  pythagtriplem8  13079  pythagtriplem9  13080  pceq0  13129  4sqlem10  13194  ballotfilemirc  13332  ennnfonelemk  13348  ennnfonelemjn  13350  ennnfonelemp1  13354  ennnfonelemim  13372  mulgnn  13987  rrgnz  14685  aprirr  14703  mvrclfi  15226  isxmet2d  15591  dvexp2  15955  dvply1  16008  logbgcd1irraplemexp  16221  perfectlem2  16317  lgsval2lem  16351  lgsval4  16361  lgsdilem  16368  lgsdir  16376  gausslemma2dlem4  16405  lgseisenlem4  16414  lgsquadlem1  16418  lgsquad2  16424  m1lgs  16426  2sqlem8a  16463  2sqlem8  16464  uhgr2edg  16669  usgr1vr  16711  vdegp1aid  16777  g0wlk0  16833  eupth2lem2dc  16922  eupth2lem3lem6fi  16934  depindlem1  16969  dichmul0orlem5  16979  dichmul0orlem6  16980  pw1ndom3lem  17241  nnsf  17271  peano4nninf  17272  exmidsbthrlem  17290  refeq  17296  trilpolemeq1  17313  qdiff  17322  dceqnconst  17334