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  4251  pwntru  4284  nndceq0  4711  frecabcl  6556  frecsuclem  6563  nnsucsssuc  6651  phpm  7040  diffisn  7068  en2eqpr  7085  fival  7153  omp1eomlem  7277  difinfsnlem  7282  difinfsn  7283  ctmlemr  7291  nninfisollemne  7314  fodjuomnilemdc  7327  exmidapne  7462  indpi  7545  nqnq0pi  7641  ltxrlt  8228  sup3exmid  9120  elnnz  9472  xrnemnf  9990  xrnepnf  9991  xrlttri3  10010  nltpnft  10027  ngtmnft  10030  xrpnfdc  10055  xrmnfdc  10056  xleaddadd  10100  fzprval  10295  fzodisjsn  10397  xqltnle  10504  fxnn0nninf  10678  iseqf1olemklt  10737  seq3f1olemqsumkj  10750  expnnval  10781  fihashelne0d  11036  xrmaxrecl  11787  fsumcl2lem  11930  fprodcl2lem  12137  dvdsle  12376  mod2eq1n2dvds  12411  nndvdslegcd  12507  gcdnncl  12509  divgcdnn  12517  sqgcd  12571  eucalgf  12598  eucalginv  12599  lcmeq0  12614  lcmgcdlem  12620  qredeu  12640  rpdvds  12642  cncongr2  12647  divnumden  12739  divdenle  12740  phibndlem  12759  phisum  12784  oddprm  12803  pythagtriplem4  12812  pythagtriplem8  12816  pythagtriplem9  12817  pceq0  12866  4sqlem10  12931  ennnfonelemk  12992  ennnfonelemjn  12994  ennnfonelemp1  12998  ennnfonelemim  13016  mulgnn  13684  rrgnz  14253  aprirr  14268  isxmet2d  15043  dvexp2  15407  dvply1  15460  logbgcd1irraplemexp  15663  perfectlem2  15695  lgsval2lem  15710  lgsval4  15720  lgsdilem  15727  lgsdir  15735  gausslemma2dlem4  15764  lgseisenlem4  15773  lgsquadlem1  15777  lgsquad2  15783  m1lgs  15785  2sqlem8a  15822  2sqlem8  15823  uhgr2edg  16025  usgr1vr  16067  g0wlk0  16142  pw1ndom3lem  16466  nnsf  16485  peano4nninf  16486  exmidsbthrlem  16504  refeq  16510  trilpolemeq1  16522  dceqnconst  16542