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

Theorem necon3bid 2324
Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon3bid.1  |-  ( ph  ->  ( A  =  B  <-> 
C  =  D ) )
Assertion
Ref Expression
necon3bid  |-  ( ph  ->  ( A  =/=  B  <->  C  =/=  D ) )

Proof of Theorem necon3bid
StepHypRef Expression
1 df-ne 2284 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3bid.1 . . 3  |-  ( ph  ->  ( A  =  B  <-> 
C  =  D ) )
32necon3bbid 2323 . 2  |-  ( ph  ->  ( -.  A  =  B  <->  C  =/=  D
) )
41, 3syl5bb 191 1  |-  ( ph  ->  ( A  =/=  B  <->  C  =/=  D ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 104    = wceq 1314    =/= wne 2283
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 586  ax-in2 587
This theorem depends on definitions:  df-bi 116  df-ne 2284
This theorem is referenced by:  nebidc  2363  addneintrd  7914  addneintr2d  7915  negne0bd  8030  negned  8034  subne0d  8046  subne0ad  8048  subneintrd  8081  subneintr2d  8083  qapne  9383  xrlttri3  9534  xaddass2  9604  sqne0  10309  fihashneq0  10492  hashnncl  10493  cjne0  10631  absne0d  10910  sqrt2irraplemnn  11763  metn0  12453
  Copyright terms: Public domain W3C validator