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 2146 | . . 3 | |
2 | 1 | notbid 656 | . 2 |
3 | df-ne 2309 | . 2 | |
4 | df-ne 2309 | . 2 | |
5 | 2, 3, 4 | 3bitr4g 222 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 104 wceq 1331 wne 2308 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-5 1423 ax-gen 1425 ax-4 1487 ax-17 1506 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-ne 2309 |
This theorem is referenced by: neeq1i 2323 neeq1d 2326 nelrdva 2891 disji2 3922 0inp0 4090 frecabcl 6296 fiintim 6817 eldju2ndl 6957 updjudhf 6964 xnn0nemnf 9051 uzn0 9341 xrnemnf 9564 xrnepnf 9565 ngtmnft 9600 xsubge0 9664 xposdif 9665 xleaddadd 9670 fztpval 9863 fiinopn 12171 |
Copyright terms: Public domain | W3C validator |