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

Theorem necon3bid 2296
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 2256 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3bid.1 . . 3  |-  ( ph  ->  ( A  =  B  <-> 
C  =  D ) )
32necon3bbid 2295 . 2  |-  ( ph  ->  ( -.  A  =  B  <->  C  =/=  D
) )
41, 3syl5bb 190 1  |-  ( ph  ->  ( A  =/=  B  <->  C  =/=  D ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 103    = wceq 1289    =/= wne 2255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580
This theorem depends on definitions:  df-bi 115  df-ne 2256
This theorem is referenced by:  nebidc  2335  addneintrd  7649  addneintr2d  7650  negne0bd  7765  negned  7769  subne0d  7781  subne0ad  7783  subneintrd  7816  subneintr2d  7818  qapne  9093  xrlttri3  9236  sqne0  9984  fihashneq0  10167  hashnncl  10168  cjne0  10306  absne0d  10584  sqrt2irraplemnn  11237
  Copyright terms: Public domain W3C validator