ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  neneqd GIF version

Theorem neneqd 2304
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
StepHypRef Expression
1 neneqd.1 . 2 (𝜑𝐴𝐵)
2 df-ne 2284 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 121 1 (𝜑 → ¬ 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1314  wne 2283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-ne 2284
This theorem is referenced by:  neneq  2305  necon2bi  2338  necon2i  2339  pm2.21ddne  2366  nelrdva  2862  neq0r  3345  0inp0  4058  pwntru  4090  nndceq0  4499  frecabcl  6262  frecsuclem  6269  nnsucsssuc  6354  phpm  6725  diffisn  6753  en2eqpr  6767  fival  6824  omp1eomlem  6945  difinfsnlem  6950  difinfsn  6951  ctmlemr  6959  fodjuomnilemdc  6982  indpi  7114  nqnq0pi  7210  ltxrlt  7794  sup3exmid  8672  elnnz  9015  xrnemnf  9504  xrnepnf  9505  xrlttri3  9523  nltpnft  9537  ngtmnft  9540  xrpnfdc  9565  xrmnfdc  9566  xleaddadd  9610  fzprval  9802  fxnn0nninf  10151  iseqf1olemklt  10198  seq3f1olemqsumkj  10211  expnnval  10236  xrmaxrecl  10964  fsumcl2lem  11107  dvdsle  11438  mod2eq1n2dvds  11472  nndvdslegcd  11550  gcdnncl  11552  divgcdnn  11559  sqgcd  11613  eucalgf  11632  eucalginv  11633  lcmeq0  11648  lcmgcdlem  11654  qredeu  11674  rpdvds  11676  cncongr2  11681  divnumden  11769  divdenle  11770  phibndlem  11787  ennnfonelemk  11808  ennnfonelemjn  11810  ennnfonelemp1  11814  ennnfonelemim  11832  isxmet2d  12412  dvexp2  12719  nnsf  13001  peano4nninf  13002  exmidsbthrlem  13019  refeq  13025  trilpolemeq1  13035
  Copyright terms: Public domain W3C validator