Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > necon3bid | Unicode version |
Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
necon3bid.1 |
Ref | Expression |
---|---|
necon3bid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2309 | . 2 | |
2 | necon3bid.1 | . . 3 | |
3 | 2 | necon3bbid 2348 | . 2 |
4 | 1, 3 | syl5bb 191 | 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 |
This theorem depends on definitions: df-bi 116 df-ne 2309 |
This theorem is referenced by: nebidc 2388 addneintrd 7950 addneintr2d 7951 negne0bd 8066 negned 8070 subne0d 8082 subne0ad 8084 subneintrd 8117 subneintr2d 8119 qapne 9431 xrlttri3 9583 xaddass2 9653 sqne0 10358 fihashneq0 10541 hashnncl 10542 cjne0 10680 absne0d 10959 sqrt2irraplemnn 11857 metn0 12547 |
Copyright terms: Public domain | W3C validator |