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  6545  frecsuclem  6552  nnsucsssuc  6638  phpm  7027  diffisn  7055  en2eqpr  7069  fival  7137  omp1eomlem  7261  difinfsnlem  7266  difinfsn  7267  ctmlemr  7275  nninfisollemne  7298  fodjuomnilemdc  7311  exmidapne  7446  indpi  7529  nqnq0pi  7625  ltxrlt  8212  sup3exmid  9104  elnnz  9456  xrnemnf  9973  xrnepnf  9974  xrlttri3  9993  nltpnft  10010  ngtmnft  10013  xrpnfdc  10038  xrmnfdc  10039  xleaddadd  10083  fzprval  10278  fzodisjsn  10380  xqltnle  10487  fxnn0nninf  10661  iseqf1olemklt  10720  seq3f1olemqsumkj  10733  expnnval  10764  fihashelne0d  11019  xrmaxrecl  11766  fsumcl2lem  11909  fprodcl2lem  12116  dvdsle  12355  mod2eq1n2dvds  12390  nndvdslegcd  12486  gcdnncl  12488  divgcdnn  12496  sqgcd  12550  eucalgf  12577  eucalginv  12578  lcmeq0  12593  lcmgcdlem  12599  qredeu  12619  rpdvds  12621  cncongr2  12626  divnumden  12718  divdenle  12719  phibndlem  12738  phisum  12763  oddprm  12782  pythagtriplem4  12791  pythagtriplem8  12795  pythagtriplem9  12796  pceq0  12845  4sqlem10  12910  ennnfonelemk  12971  ennnfonelemjn  12973  ennnfonelemp1  12977  ennnfonelemim  12995  mulgnn  13663  rrgnz  14232  aprirr  14247  isxmet2d  15022  dvexp2  15386  dvply1  15439  logbgcd1irraplemexp  15642  perfectlem2  15674  lgsval2lem  15689  lgsval4  15699  lgsdilem  15706  lgsdir  15714  gausslemma2dlem4  15743  lgseisenlem4  15752  lgsquadlem1  15756  lgsquad2  15762  m1lgs  15764  2sqlem8a  15801  2sqlem8  15802  uhgr2edg  16004  g0wlk0  16081  nnsf  16371  peano4nninf  16372  exmidsbthrlem  16390  refeq  16396  trilpolemeq1  16408  dceqnconst  16428