Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > necon3d | Unicode version |
Description: Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.) |
Ref | Expression |
---|---|
necon3d.1 |
Ref | Expression |
---|---|
necon3d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3d.1 | . . 3 | |
2 | 1 | necon3ad 2382 | . 2 |
3 | df-ne 2341 | . 2 | |
4 | 2, 3 | syl6ibr 161 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wceq 1348 wne 2340 |
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 609 ax-in2 610 |
This theorem depends on definitions: df-bi 116 df-ne 2341 |
This theorem is referenced by: necon3i 2388 pm13.18 2421 ssn0 3456 suppssfv 6055 suppssov1 6056 nnmord 6494 findcard2 6865 findcard2s 6866 addn0nid 8286 nn0n0n1ge2 9275 xnegdi 9818 efne0 11634 divgcdcoprmex 12049 pceulem 12241 pcqmul 12250 pcqcl 12253 pcaddlem 12285 pcadd 12286 |
Copyright terms: Public domain | W3C validator |