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  3010  neq0r  3506  ifnetruedc  3646  ifnefals  3647  0inp0  4250  pwntru  4283  nndceq0  4710  frecabcl  6551  frecsuclem  6558  nnsucsssuc  6646  phpm  7035  diffisn  7063  en2eqpr  7080  fival  7148  omp1eomlem  7272  difinfsnlem  7277  difinfsn  7278  ctmlemr  7286  nninfisollemne  7309  fodjuomnilemdc  7322  exmidapne  7457  indpi  7540  nqnq0pi  7636  ltxrlt  8223  sup3exmid  9115  elnnz  9467  xrnemnf  9985  xrnepnf  9986  xrlttri3  10005  nltpnft  10022  ngtmnft  10025  xrpnfdc  10050  xrmnfdc  10051  xleaddadd  10095  fzprval  10290  fzodisjsn  10392  xqltnle  10499  fxnn0nninf  10673  iseqf1olemklt  10732  seq3f1olemqsumkj  10745  expnnval  10776  fihashelne0d  11031  xrmaxrecl  11782  fsumcl2lem  11925  fprodcl2lem  12132  dvdsle  12371  mod2eq1n2dvds  12406  nndvdslegcd  12502  gcdnncl  12504  divgcdnn  12512  sqgcd  12566  eucalgf  12593  eucalginv  12594  lcmeq0  12609  lcmgcdlem  12615  qredeu  12635  rpdvds  12637  cncongr2  12642  divnumden  12734  divdenle  12735  phibndlem  12754  phisum  12779  oddprm  12798  pythagtriplem4  12807  pythagtriplem8  12811  pythagtriplem9  12812  pceq0  12861  4sqlem10  12926  ennnfonelemk  12987  ennnfonelemjn  12989  ennnfonelemp1  12993  ennnfonelemim  13011  mulgnn  13679  rrgnz  14248  aprirr  14263  isxmet2d  15038  dvexp2  15402  dvply1  15455  logbgcd1irraplemexp  15658  perfectlem2  15690  lgsval2lem  15705  lgsval4  15715  lgsdilem  15722  lgsdir  15730  gausslemma2dlem4  15759  lgseisenlem4  15768  lgsquadlem1  15772  lgsquad2  15778  m1lgs  15780  2sqlem8a  15817  2sqlem8  15818  uhgr2edg  16020  g0wlk0  16116  pw1ndom3lem  16440  nnsf  16459  peano4nninf  16460  exmidsbthrlem  16478  refeq  16484  trilpolemeq1  16496  dceqnconst  16516