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  2946  neq0r  3439  0inp0  4168  pwntru  4201  nndceq0  4619  frecabcl  6403  frecsuclem  6410  nnsucsssuc  6496  phpm  6868  diffisn  6896  en2eqpr  6910  fival  6972  omp1eomlem  7096  difinfsnlem  7101  difinfsn  7102  ctmlemr  7110  nninfisollemne  7132  fodjuomnilemdc  7145  exmidapne  7262  indpi  7344  nqnq0pi  7440  ltxrlt  8026  sup3exmid  8917  elnnz  9266  xrnemnf  9780  xrnepnf  9781  xrlttri3  9800  nltpnft  9817  ngtmnft  9820  xrpnfdc  9845  xrmnfdc  9846  xleaddadd  9890  fzprval  10085  fxnn0nninf  10441  iseqf1olemklt  10488  seq3f1olemqsumkj  10501  expnnval  10526  fihashelne0d  10780  xrmaxrecl  11266  fsumcl2lem  11409  fprodcl2lem  11616  dvdsle  11853  mod2eq1n2dvds  11887  nndvdslegcd  11969  gcdnncl  11971  divgcdnn  11979  sqgcd  12033  eucalgf  12058  eucalginv  12059  lcmeq0  12074  lcmgcdlem  12080  qredeu  12100  rpdvds  12102  cncongr2  12107  divnumden  12199  divdenle  12200  phibndlem  12219  phisum  12243  oddprm  12262  pythagtriplem4  12271  pythagtriplem8  12275  pythagtriplem9  12276  pceq0  12324  4sqlem10  12388  ennnfonelemk  12404  ennnfonelemjn  12406  ennnfonelemp1  12410  ennnfonelemim  12428  mulgnn  13003  aprirr  13411  isxmet2d  14036  dvexp2  14364  logbgcd1irraplemexp  14574  lgsval2lem  14599  lgsval4  14609  lgsdilem  14616  lgsdir  14624  m1lgs  14640  2sqlem8a  14657  2sqlem8  14658  nnsf  14943  peano4nninf  14944  exmidsbthrlem  14959  refeq  14965  trilpolemeq1  14977  dceqnconst  14997