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

Theorem neeq1d 2326
 Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
Hypothesis
Ref Expression
neeq1d.1
Assertion
Ref Expression
neeq1d

Proof of Theorem neeq1d
StepHypRef Expression
1 neeq1d.1 . 2
2 neeq1 2321 . 2
31, 2syl 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104   wceq 1331   wne 2308 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-ne 2309 This theorem is referenced by:  neeq12d  2328  eqnetrd  2332  prnzg  3647  hashprg  10561  algcvg  11736  algcvga  11739  eucalgcvga  11746  rpdvds  11787  phibndlem  11899  dfphi2  11903  ennnfoneleminc  11931  ennnfonelemex  11934  ennnfonelemhom  11935  ennnfonelemnn0  11942  ennnfonelemr  11943  ennnfonelemim  11944  ctinfomlemom  11947
 Copyright terms: Public domain W3C validator