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  3707  hashprg  10743  algcvg  12002  algcvga  12005  eucalgcvga  12012  rpdvds  12053  phibndlem  12170  dfphi2  12174  pcaddlem  12292  ennnfoneleminc  12366  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemnn0  12377  ennnfonelemr  12378  ennnfonelemim  12379  ctinfomlemom  12382  lgsne0  13733  dceqnconst  14091  dcapnconst  14092  nconstwlpolem  14096
  Copyright terms: Public domain W3C validator