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

Theorem neqned 2262
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2276. One-way deduction form of df-ne 2256. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2305. (Revised by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
neqned.1  |-  ( ph  ->  -.  A  =  B )
Assertion
Ref Expression
neqned  |-  ( ph  ->  A  =/=  B )

Proof of Theorem neqned
StepHypRef Expression
1 neqned.1 . 2  |-  ( ph  ->  -.  A  =  B )
2 df-ne 2256 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylibr 132 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = 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
This theorem depends on definitions:  df-bi 115  df-ne 2256
This theorem is referenced by:  neqne  2263  tfr1onlemsucaccv  6088  tfrcllemsucaccv  6101  djune  6748  flqltnz  9659  zfz1iso  10210  bezoutlemle  11077  eucalgval2  11115  eucalglt  11119  lcmval  11125  lcmcllem  11129  isprm2  11179  sqne2sq  11235  nnsf  11539  peano3nninf  11541
  Copyright terms: Public domain W3C validator