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

Theorem necon3bid 2290
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 2250 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3bid.1 . . 3  |-  ( ph  ->  ( A  =  B  <-> 
C  =  D ) )
32necon3bbid 2289 . 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 1285    =/= wne 2249
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 577  ax-in2 578
This theorem depends on definitions:  df-bi 115  df-ne 2250
This theorem is referenced by:  nebidc  2329  addneintrd  7573  addneintr2d  7574  negne0bd  7689  negned  7693  subne0d  7705  subne0ad  7707  subneintrd  7740  subneintr2d  7742  qapne  9019  xrlttri3  9162  sqne0  9857  fihashneq0  10038  hashnncl  10039  cjne0  10169  absne0d  10447  sqrt2irraplemnn  10937
  Copyright terms: Public domain W3C validator