![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > neqned | Unicode version |
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2330. One-way deduction form of df-ne 2310. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2359. (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 2310 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylibr 133 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 2310 |
This theorem is referenced by: neqne 2317 tfr1onlemsucaccv 6246 tfrcllemsucaccv 6259 enpr2d 6719 djune 6971 omp1eomlem 6987 difinfsn 6993 xaddf 9657 xaddval 9658 xleaddadd 9700 flqltnz 10091 zfz1iso 10616 bezoutlemle 11732 eucalgval2 11770 eucalglt 11774 lcmval 11780 lcmcllem 11784 isprm2 11834 sqne2sq 11891 ennnfonelemim 11973 ctinfomlemom 11976 logbgcd1irraplemexp 13093 nnsf 13374 peano3nninf 13376 neapmkvlem 13424 |
Copyright terms: Public domain | W3C validator |