![]() |
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 2184 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | notbid 667 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-ne 2348 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-ne 2348 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3bitr4g 223 |
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 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-ne 2348 |
This theorem is referenced by: neeq1i 2362 neeq1d 2365 nelrdva 2946 disji2 3998 0inp0 4168 frecabcl 6402 fiintim 6930 eldju2ndl 7073 updjudhf 7080 netap 7255 2oneel 7257 2omotaplemap 7258 2omotaplemst 7259 exmidapne 7261 xnn0nemnf 9252 uzn0 9545 xrnemnf 9779 xrnepnf 9780 ngtmnft 9819 xsubge0 9883 xposdif 9884 xleaddadd 9889 fztpval 10085 pcpre1 12294 pcqmul 12305 pcqcl 12308 xpsfrnel 12768 fiinopn 13589 neapmkv 14901 neap0mkv 14902 ltlenmkv 14903 |
Copyright terms: Public domain | W3C validator |