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

Theorem neneqd 2276
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 2256 . 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 1289    =/= wne 2255
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 2256
This theorem is referenced by:  neneq  2277  necon2bi  2310  necon2i  2311  pm2.21ddne  2338  nelrdva  2820  neq0r  3295  0inp0  3993  nndceq0  4421  frecabcl  6146  frecsuclem  6153  nnsucsssuc  6235  phpm  6561  diffisn  6589  en2eqpr  6603  fodjuomnilemdc  6778  indpi  6880  nqnq0pi  6976  ltxrlt  7531  elnnz  8730  xrnemnf  9217  xrnepnf  9218  xrlttri3  9236  nltpnft  9248  ngtmnft  9249  fzprval  9463  fxnn0nninf  9809  iseqf1olemklt  9879  seq3f1olemqsumkj  9892  expnnval  9923  fsumcl2lem  10755  dvdsle  10927  mod2eq1n2dvds  10961  nndvdslegcd  11039  gcdnncl  11041  divgcdnn  11048  sqgcd  11100  eucalgf  11119  eucalginv  11120  lcmeq0  11135  lcmgcdlem  11141  qredeu  11161  rpdvds  11163  cncongr2  11168  divnumden  11256  divdenle  11257  phibndlem  11274  nnsf  11541  peano4nninf  11542  exmidsbthrlem  11558
  Copyright terms: Public domain W3C validator