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

Theorem neqned 2315
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2329. One-way deduction form of df-ne 2309. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2358. (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 2309 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylibr 133 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = 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
This theorem depends on definitions:  df-bi 116  df-ne 2309
This theorem is referenced by:  neqne  2316  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  enpr2d  6711  djune  6963  omp1eomlem  6979  difinfsn  6985  xaddf  9627  xaddval  9628  xleaddadd  9670  flqltnz  10060  zfz1iso  10584  bezoutlemle  11696  eucalgval2  11734  eucalglt  11738  lcmval  11744  lcmcllem  11748  isprm2  11798  sqne2sq  11855  ennnfonelemim  11937  ctinfomlemom  11940  nnsf  13199  peano3nninf  13201
  Copyright terms: Public domain W3C validator