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

Theorem neeq1d 2378
Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
Hypothesis
Ref Expression
neeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
neeq1d  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )

Proof of Theorem neeq1d
StepHypRef Expression
1 neeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 neeq1 2373 . 2  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2syl 14 1  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    = wceq 1364    =/= wne 2360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-ne 2361
This theorem is referenced by:  neeq12d  2380  eqnetrd  2384  prnzg  3731  pw2f1odclem  6862  hashprg  10820  algcvg  12080  algcvga  12083  eucalgcvga  12090  rpdvds  12131  phibndlem  12248  dfphi2  12252  pcaddlem  12371  ennnfoneleminc  12462  ennnfonelemex  12465  ennnfonelemhom  12466  ennnfonelemnn0  12473  ennnfonelemr  12474  ennnfonelemim  12475  ctinfomlemom  12478  setscomd  12553  lgsne0  14897  dceqnconst  15267  dcapnconst  15268  nconstwlpolem  15272
  Copyright terms: Public domain W3C validator