Theorem neneqd 2388

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1364   ≠ wne 2367

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 2368

This theorem is referenced by:  neneq  2389  necon2bi  2422  necon2i  2423  pm2.21ddne  2450  nelrdva  2971  neq0r  3465  ifnetruedc  3602  ifnefals  3603  0inp0  4199  pwntru  4232  nndceq0  4654  frecabcl  6457  frecsuclem  6464  nnsucsssuc  6550  phpm  6926  diffisn  6954  en2eqpr  6968  fival  7036  omp1eomlem  7160  difinfsnlem  7165  difinfsn  7166  ctmlemr  7174  nninfisollemne  7197  fodjuomnilemdc  7210  exmidapne  7327  indpi  7409  nqnq0pi  7505  ltxrlt  8092  sup3exmid  8984  elnnz  9336  xrnemnf  9852  xrnepnf  9853  xrlttri3  9872  nltpnft  9889  ngtmnft  9892  xrpnfdc  9917  xrmnfdc  9918  xleaddadd  9962  fzprval  10157  xqltnle  10357  fxnn0nninf  10531  iseqf1olemklt  10590  seq3f1olemqsumkj  10603  expnnval  10634  fihashelne0d  10889  xrmaxrecl  11420  fsumcl2lem  11563  fprodcl2lem  11770  dvdsle  12009  mod2eq1n2dvds  12044  nndvdslegcd  12132  gcdnncl  12134  divgcdnn  12142  sqgcd  12196  eucalgf  12223  eucalginv  12224  lcmeq0  12239  lcmgcdlem  12245  qredeu  12265  rpdvds  12267  cncongr2  12272  divnumden  12364  divdenle  12365  phibndlem  12384  phisum  12409  oddprm  12428  pythagtriplem4  12437  pythagtriplem8  12441  pythagtriplem9  12442  pceq0  12491  4sqlem10  12556  ennnfonelemk  12617  ennnfonelemjn  12619  ennnfonelemp1  12623  ennnfonelemim  12641  mulgnn  13256  rrgnz  13824  aprirr  13839  isxmet2d  14584  dvexp2  14948  dvply1  15001  logbgcd1irraplemexp  15204  perfectlem2  15236  lgsval2lem  15251  lgsval4  15261  lgsdilem  15268  lgsdir  15276  gausslemma2dlem4  15305  lgseisenlem4  15314  lgsquadlem1  15318  lgsquad2  15324  m1lgs  15326  2sqlem8a  15363  2sqlem8  15364  nnsf  15649  peano4nninf  15650  exmidsbthrlem  15666  refeq  15672  trilpolemeq1  15684  dceqnconst  15704