Theorem neneqd 2441

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  neneq  2442  necon2bi  2475  necon2i  2476  pm2.21ddne  2503  nelrdva  3033  neq0r  3536  ifnetruedc  3684  ifnefals  3685  0inp0  4303  pwntru  4336  nndceq0  4765  fczsupp0  6499  frecabcl  6670  frecsuclem  6677  nnsucsssuc  6765  phpm  7167  diffisn  7197  en2eqpr  7214  fival  7304  omp1eomlem  7435  difinfsnlem  7440  difinfsn  7441  ctmlemr  7449  nninfisollemne  7472  fodjuomnilemdc  7485  exmidapne  7627  indpi  7710  nqnq0pi  7806  ltxrlt  8392  sup3exmid  9290  elnnz  9659  xrnemnf  10190  xrnepnf  10191  xrlttri3  10210  nltpnft  10227  ngtmnft  10230  xrpnfdc  10255  xrmnfdc  10256  xleaddadd  10300  fzprval  10500  fzodisjsn  10602  xqltnle  10713  fxnn0nninf  10891  iseqf1olemklt  10950  seq3f1olemqsumkj  10963  expnnval  10994  fihashelne0d  11252  xrmaxrecl  12040  fsumcl2lem  12184  fprodcl2lem  12391  dvdsle  12630  mod2eq1n2dvds  12665  nndvdslegcd  12761  gcdnncl  12763  divgcdnn  12771  sqgcd  12825  eucalgf  12852  eucalginv  12853  lcmeq0  12868  lcmgcdlem  12874  qredeu  12894  rpdvds  12896  cncongr2  12901  divnumden  12995  divdenle  12996  phibndlem  13017  phisum  13042  oddprm  13061  pythagtriplem4  13070  pythagtriplem8  13074  pythagtriplem9  13075  pceq0  13124  4sqlem10  13189  ballotfilemirc  13327  ennnfonelemk  13343  ennnfonelemjn  13345  ennnfonelemp1  13349  ennnfonelemim  13367  mulgnn  13982  rrgnz  14661  aprirr  14679  isxmet2d  15540  dvexp2  15904  dvply1  15957  logbgcd1irraplemexp  16165  perfectlem2  16261  lgsval2lem  16295  lgsval4  16305  lgsdilem  16312  lgsdir  16320  gausslemma2dlem4  16349  lgseisenlem4  16358  lgsquadlem1  16362  lgsquad2  16368  m1lgs  16370  2sqlem8a  16407  2sqlem8  16408  uhgr2edg  16613  usgr1vr  16655  vdegp1aid  16721  g0wlk0  16777  eupth2lem2dc  16866  eupth2lem3lem6fi  16878  depindlem1  16913  dichmul0orlem5  16923  dichmul0orlem6  16924  pw1ndom3lem  17185  nnsf  17214  peano4nninf  17215  exmidsbthrlem  17233  refeq  17239  trilpolemeq1  17256  qdiff  17265  dceqnconst  17277