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

Theorem neneqd 2267
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 2247 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylib 120 1  |-  ( ph  ->  -.  A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1285    =/= wne 2246
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-ne 2247
This theorem is referenced by:  neneq  2268  necon2bi  2301  necon2i  2302  pm2.21ddne  2329  nelrdva  2798  neq0r  3269  0inp0  3948  nndceq0  4365  frecabcl  6048  frecsuclem  6055  nnsucsssuc  6136  phpm  6400  diffisn  6427  en2eqpr  6434  indpi  6594  nqnq0pi  6690  ltxrlt  7245  elnnz  8442  xrnemnf  8929  xrnepnf  8930  xrlttri3  8948  nltpnft  8960  ngtmnft  8961  fzprval  9175  expival  9575  expinnval  9576  dvdsle  10389  mod2eq1n2dvds  10423  nndvdslegcd  10501  gcdnncl  10503  divgcdnn  10510  sqgcd  10562  eucalgf  10581  eucalginv  10582  lcmeq0  10597  lcmgcdlem  10603  qredeu  10623  rpdvds  10625  cncongr2  10630
  Copyright terms: Public domain W3C validator