ILE Home 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  |-  ( 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 2321 . 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 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