ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  neqned GIF 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 (𝜑 → ¬ 𝐴 = 𝐵)
Assertion
Ref Expression
neqned (𝜑𝐴𝐵)

Proof of Theorem neqned
StepHypRef Expression
1 neqned.1 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
2 df-ne 2256 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylibr 132 1 (𝜑𝐴𝐵)
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  10211  bezoutlemle  11079  eucalgval2  11117  eucalglt  11121  lcmval  11127  lcmcllem  11131  isprm2  11181  sqne2sq  11237  nnsf  11541  peano3nninf  11543
  Copyright terms: Public domain W3C validator