Theorem neneqd 2421

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1395   ≠ wne 2400

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 2401

This theorem is referenced by:  neneq  2422  necon2bi  2455  necon2i  2456  pm2.21ddne  2483  nelrdva  3011  neq0r  3507  ifnetruedc  3647  ifnefals  3648  0inp0  4254  pwntru  4287  nndceq0  4714  frecabcl  6560  frecsuclem  6567  nnsucsssuc  6655  phpm  7047  diffisn  7075  en2eqpr  7092  fival  7160  omp1eomlem  7284  difinfsnlem  7289  difinfsn  7290  ctmlemr  7298  nninfisollemne  7321  fodjuomnilemdc  7334  exmidapne  7469  indpi  7552  nqnq0pi  7648  ltxrlt  8235  sup3exmid  9127  elnnz  9479  xrnemnf  10002  xrnepnf  10003  xrlttri3  10022  nltpnft  10039  ngtmnft  10042  xrpnfdc  10067  xrmnfdc  10068  xleaddadd  10112  fzprval  10307  fzodisjsn  10409  xqltnle  10517  fxnn0nninf  10691  iseqf1olemklt  10750  seq3f1olemqsumkj  10763  expnnval  10794  fihashelne0d  11049  xrmaxrecl  11806  fsumcl2lem  11949  fprodcl2lem  12156  dvdsle  12395  mod2eq1n2dvds  12430  nndvdslegcd  12526  gcdnncl  12528  divgcdnn  12536  sqgcd  12590  eucalgf  12617  eucalginv  12618  lcmeq0  12633  lcmgcdlem  12639  qredeu  12659  rpdvds  12661  cncongr2  12666  divnumden  12758  divdenle  12759  phibndlem  12778  phisum  12803  oddprm  12822  pythagtriplem4  12831  pythagtriplem8  12835  pythagtriplem9  12836  pceq0  12885  4sqlem10  12950  ennnfonelemk  13011  ennnfonelemjn  13013  ennnfonelemp1  13017  ennnfonelemim  13035  mulgnn  13703  rrgnz  14272  aprirr  14287  isxmet2d  15062  dvexp2  15426  dvply1  15479  logbgcd1irraplemexp  15682  perfectlem2  15714  lgsval2lem  15729  lgsval4  15739  lgsdilem  15746  lgsdir  15754  gausslemma2dlem4  15783  lgseisenlem4  15792  lgsquadlem1  15796  lgsquad2  15802  m1lgs  15804  2sqlem8a  15841  2sqlem8  15842  uhgr2edg  16045  usgr1vr  16087  g0wlk0  16167  pw1ndom3lem  16524  nnsf  16543  peano4nninf  16544  exmidsbthrlem  16562  refeq  16568  trilpolemeq1  16580  dceqnconst  16600