Theorem neneqd 2423

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1397   ≠ wne 2402

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 2403

This theorem is referenced by:  neneq  2424  necon2bi  2457  necon2i  2458  pm2.21ddne  2485  nelrdva  3013  neq0r  3509  ifnetruedc  3649  ifnefals  3650  0inp0  4256  pwntru  4289  nndceq0  4716  frecabcl  6564  frecsuclem  6571  nnsucsssuc  6659  phpm  7051  diffisn  7081  en2eqpr  7098  fival  7168  omp1eomlem  7292  difinfsnlem  7297  difinfsn  7298  ctmlemr  7306  nninfisollemne  7329  fodjuomnilemdc  7342  exmidapne  7478  indpi  7561  nqnq0pi  7657  ltxrlt  8244  sup3exmid  9136  elnnz  9488  xrnemnf  10011  xrnepnf  10012  xrlttri3  10031  nltpnft  10048  ngtmnft  10051  xrpnfdc  10076  xrmnfdc  10077  xleaddadd  10121  fzprval  10316  fzodisjsn  10418  xqltnle  10526  fxnn0nninf  10700  iseqf1olemklt  10759  seq3f1olemqsumkj  10772  expnnval  10803  fihashelne0d  11058  xrmaxrecl  11815  fsumcl2lem  11958  fprodcl2lem  12165  dvdsle  12404  mod2eq1n2dvds  12439  nndvdslegcd  12535  gcdnncl  12537  divgcdnn  12545  sqgcd  12599  eucalgf  12626  eucalginv  12627  lcmeq0  12642  lcmgcdlem  12648  qredeu  12668  rpdvds  12670  cncongr2  12675  divnumden  12767  divdenle  12768  phibndlem  12787  phisum  12812  oddprm  12831  pythagtriplem4  12840  pythagtriplem8  12844  pythagtriplem9  12845  pceq0  12894  4sqlem10  12959  ennnfonelemk  13020  ennnfonelemjn  13022  ennnfonelemp1  13026  ennnfonelemim  13044  mulgnn  13712  rrgnz  14281  aprirr  14296  isxmet2d  15071  dvexp2  15435  dvply1  15488  logbgcd1irraplemexp  15691  perfectlem2  15723  lgsval2lem  15738  lgsval4  15748  lgsdilem  15755  lgsdir  15763  gausslemma2dlem4  15792  lgseisenlem4  15801  lgsquadlem1  15805  lgsquad2  15811  m1lgs  15813  2sqlem8a  15850  2sqlem8  15851  uhgr2edg  16056  usgr1vr  16098  vdegp1aid  16164  g0wlk0  16220  eupth2lem2dc  16309  pw1ndom3lem  16588  nnsf  16607  peano4nninf  16608  exmidsbthrlem  16626  refeq  16632  trilpolemeq1  16644  dceqnconst  16664