Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > neneqd | Unicode version |
Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
neneqd.1 |
Ref | Expression |
---|---|
neneqd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neneqd.1 | . 2 | |
2 | df-ne 2286 | . 2 | |
3 | 1, 2 | sylib 121 | 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 |
This theorem depends on definitions: df-bi 116 df-ne 2286 |
This theorem is referenced by: neneq 2307 necon2bi 2340 necon2i 2341 pm2.21ddne 2368 nelrdva 2864 neq0r 3347 0inp0 4060 pwntru 4092 nndceq0 4501 frecabcl 6264 frecsuclem 6271 nnsucsssuc 6356 phpm 6727 diffisn 6755 en2eqpr 6769 fival 6826 omp1eomlem 6947 difinfsnlem 6952 difinfsn 6953 ctmlemr 6961 fodjuomnilemdc 6984 indpi 7118 nqnq0pi 7214 ltxrlt 7798 sup3exmid 8683 elnnz 9032 xrnemnf 9532 xrnepnf 9533 xrlttri3 9551 nltpnft 9565 ngtmnft 9568 xrpnfdc 9593 xrmnfdc 9594 xleaddadd 9638 fzprval 9830 fxnn0nninf 10179 iseqf1olemklt 10226 seq3f1olemqsumkj 10239 expnnval 10264 xrmaxrecl 10992 fsumcl2lem 11135 dvdsle 11469 mod2eq1n2dvds 11503 nndvdslegcd 11581 gcdnncl 11583 divgcdnn 11590 sqgcd 11644 eucalgf 11663 eucalginv 11664 lcmeq0 11679 lcmgcdlem 11685 qredeu 11705 rpdvds 11707 cncongr2 11712 divnumden 11801 divdenle 11802 phibndlem 11819 ennnfonelemk 11840 ennnfonelemjn 11842 ennnfonelemp1 11846 ennnfonelemim 11864 isxmet2d 12444 dvexp2 12772 nnsf 13126 peano4nninf 13127 exmidsbthrlem 13144 refeq 13150 trilpolemeq1 13160 |
Copyright terms: Public domain | W3C validator |