Theorem neneqd 2348

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1335   ≠ wne 2327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-ne 2328

This theorem is referenced by:  neneq  2349  necon2bi  2382  necon2i  2383  pm2.21ddne  2410  nelrdva  2919  neq0r  3408  0inp0  4126  pwntru  4159  nndceq0  4575  frecabcl  6340  frecsuclem  6347  nnsucsssuc  6432  phpm  6803  diffisn  6831  en2eqpr  6845  fival  6907  omp1eomlem  7028  difinfsnlem  7033  difinfsn  7034  ctmlemr  7042  fodjuomnilemdc  7070  indpi  7245  nqnq0pi  7341  ltxrlt  7926  sup3exmid  8811  elnnz  9160  xrnemnf  9666  xrnepnf  9667  xrlttri3  9686  nltpnft  9700  ngtmnft  9703  xrpnfdc  9728  xrmnfdc  9729  xleaddadd  9773  fzprval  9966  fxnn0nninf  10319  iseqf1olemklt  10366  seq3f1olemqsumkj  10379  expnnval  10404  xrmaxrecl  11134  fsumcl2lem  11277  fprodcl2lem  11484  dvdsle  11717  mod2eq1n2dvds  11751  nndvdslegcd  11829  gcdnncl  11831  divgcdnn  11839  sqgcd  11893  eucalgf  11912  eucalginv  11913  lcmeq0  11928  lcmgcdlem  11934  qredeu  11954  rpdvds  11956  cncongr2  11961  divnumden  12050  divdenle  12051  phibndlem  12068  phisum  12092  ennnfonelemk  12101  ennnfonelemjn  12103  ennnfonelemp1  12107  ennnfonelemim  12125  isxmet2d  12708  dvexp2  13036  logbgcd1irraplemexp  13245  nnsf  13538  peano4nninf  13539  exmidsbthrlem  13555  refeq  13561  trilpolemeq1  13573  dceqnconst  13592