Theorem neneqd 2397

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1373   ≠ wne 2376

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 2377

This theorem is referenced by:  neneq  2398  necon2bi  2431  necon2i  2432  pm2.21ddne  2459  nelrdva  2980  neq0r  3475  ifnetruedc  3613  ifnefals  3614  0inp0  4211  pwntru  4244  nndceq0  4667  frecabcl  6487  frecsuclem  6494  nnsucsssuc  6580  phpm  6964  diffisn  6992  en2eqpr  7006  fival  7074  omp1eomlem  7198  difinfsnlem  7203  difinfsn  7204  ctmlemr  7212  nninfisollemne  7235  fodjuomnilemdc  7248  exmidapne  7374  indpi  7457  nqnq0pi  7553  ltxrlt  8140  sup3exmid  9032  elnnz  9384  xrnemnf  9901  xrnepnf  9902  xrlttri3  9921  nltpnft  9938  ngtmnft  9941  xrpnfdc  9966  xrmnfdc  9967  xleaddadd  10011  fzprval  10206  xqltnle  10412  fxnn0nninf  10586  iseqf1olemklt  10645  seq3f1olemqsumkj  10658  expnnval  10689  fihashelne0d  10944  xrmaxrecl  11599  fsumcl2lem  11742  fprodcl2lem  11949  dvdsle  12188  mod2eq1n2dvds  12223  nndvdslegcd  12319  gcdnncl  12321  divgcdnn  12329  sqgcd  12383  eucalgf  12410  eucalginv  12411  lcmeq0  12426  lcmgcdlem  12432  qredeu  12452  rpdvds  12454  cncongr2  12459  divnumden  12551  divdenle  12552  phibndlem  12571  phisum  12596  oddprm  12615  pythagtriplem4  12624  pythagtriplem8  12628  pythagtriplem9  12629  pceq0  12678  4sqlem10  12743  ennnfonelemk  12804  ennnfonelemjn  12806  ennnfonelemp1  12810  ennnfonelemim  12828  mulgnn  13495  rrgnz  14063  aprirr  14078  isxmet2d  14853  dvexp2  15217  dvply1  15270  logbgcd1irraplemexp  15473  perfectlem2  15505  lgsval2lem  15520  lgsval4  15530  lgsdilem  15537  lgsdir  15545  gausslemma2dlem4  15574  lgseisenlem4  15583  lgsquadlem1  15587  lgsquad2  15593  m1lgs  15595  2sqlem8a  15632  2sqlem8  15633  nnsf  15979  peano4nninf  15980  exmidsbthrlem  15998  refeq  16004  trilpolemeq1  16016  dceqnconst  16036