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

Theorem neqned 2292
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2306. One-way deduction form of df-ne 2286. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2335. (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 2286 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylibr 133 1 (𝜑𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1316  wne 2285
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 2286
This theorem is referenced by:  neqne  2293  tfr1onlemsucaccv  6206  tfrcllemsucaccv  6219  enpr2d  6679  djune  6931  omp1eomlem  6947  difinfsn  6953  xaddf  9595  xaddval  9596  xleaddadd  9638  flqltnz  10028  zfz1iso  10552  bezoutlemle  11623  eucalgval2  11661  eucalglt  11665  lcmval  11671  lcmcllem  11675  isprm2  11725  sqne2sq  11782  ennnfonelemim  11864  ctinfomlemom  11867  nnsf  13126  peano3nninf  13128
  Copyright terms: Public domain W3C validator