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

Theorem neeq1d 2358
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 2353 . 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 104    = wceq 1348    =/= wne 2340
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 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341
This theorem is referenced by:  neeq12d  2360  eqnetrd  2364  prnzg  3705  hashprg  10730  algcvg  11989  algcvga  11992  eucalgcvga  11999  rpdvds  12040  phibndlem  12157  dfphi2  12161  pcaddlem  12279  ennnfoneleminc  12353  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemnn0  12364  ennnfonelemr  12365  ennnfonelemim  12366  ctinfomlemom  12369  lgsne0  13654  dceqnconst  14013  dcapnconst  14014  nconstwlpolem  14018
  Copyright terms: Public domain W3C validator