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

Theorem neneqd 2306
Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
neneqd.1  |-  ( ph  ->  A  =/=  B )
Assertion
Ref Expression
neneqd  |-  ( ph  ->  -.  A  =  B )

Proof of Theorem neneqd
StepHypRef Expression
1 neneqd.1 . 2  |-  ( ph  ->  A  =/=  B )
2 df-ne 2286 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylib 121 1  |-  ( ph  ->  -.  A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1316    =/= wne 2285
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 2286
This theorem is referenced by:  neneq  2307  necon2bi  2340  necon2i  2341  pm2.21ddne  2368  nelrdva  2864  neq0r  3347  0inp0  4060  pwntru  4092  nndceq0  4501  frecabcl  6264  frecsuclem  6271  nnsucsssuc  6356  phpm  6727  diffisn  6755  en2eqpr  6769  fival  6826  omp1eomlem  6947  difinfsnlem  6952  difinfsn  6953  ctmlemr  6961  fodjuomnilemdc  6984  indpi  7118  nqnq0pi  7214  ltxrlt  7798  sup3exmid  8683  elnnz  9032  xrnemnf  9532  xrnepnf  9533  xrlttri3  9551  nltpnft  9565  ngtmnft  9568  xrpnfdc  9593  xrmnfdc  9594  xleaddadd  9638  fzprval  9830  fxnn0nninf  10179  iseqf1olemklt  10226  seq3f1olemqsumkj  10239  expnnval  10264  xrmaxrecl  10992  fsumcl2lem  11135  dvdsle  11469  mod2eq1n2dvds  11503  nndvdslegcd  11581  gcdnncl  11583  divgcdnn  11590  sqgcd  11644  eucalgf  11663  eucalginv  11664  lcmeq0  11679  lcmgcdlem  11685  qredeu  11705  rpdvds  11707  cncongr2  11712  divnumden  11801  divdenle  11802  phibndlem  11819  ennnfonelemk  11840  ennnfonelemjn  11842  ennnfonelemp1  11846  ennnfonelemim  11864  isxmet2d  12444  dvexp2  12772  nnsf  13126  peano4nninf  13127  exmidsbthrlem  13144  refeq  13150  trilpolemeq1  13160
  Copyright terms: Public domain W3C validator