![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > neeq1 | Unicode version |
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) |
Ref | Expression |
---|---|
neeq1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2121 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | notbid 639 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-ne 2283 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-ne 2283 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3bitr4g 222 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-5 1406 ax-gen 1408 ax-4 1470 ax-17 1489 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-cleq 2108 df-ne 2283 |
This theorem is referenced by: neeq1i 2297 neeq1d 2300 nelrdva 2860 disji2 3888 0inp0 4050 frecabcl 6250 fiintim 6770 eldju2ndl 6909 updjudhf 6916 xnn0nemnf 8955 uzn0 9243 xrnemnf 9457 xrnepnf 9458 ngtmnft 9493 xsubge0 9557 xposdif 9558 xleaddadd 9563 fztpval 9756 fiinopn 12014 |
Copyright terms: Public domain | W3C validator |