Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > neqned | GIF version |
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.) |
Ref | Expression |
---|---|
neqned.1 | ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
Ref | Expression |
---|---|
neqned | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neqned.1 | . 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵) | |
2 | df-ne 2286 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | sylibr 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 |