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

Proof of Theorem neqned
StepHypRef Expression
1 neqned.1 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
2 df-ne 2309 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylibr 133 1 (𝜑𝐴𝐵)
 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  9634  xaddval  9635  xleaddadd  9677  flqltnz  10067  zfz1iso  10591  bezoutlemle  11702  eucalgval2  11740  eucalglt  11744  lcmval  11750  lcmcllem  11754  isprm2  11804  sqne2sq  11861  ennnfonelemim  11943  ctinfomlemom  11946  nnsf  13252  peano3nninf  13254
 Copyright terms: Public domain W3C validator