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 3457 suppssfv 6057 suppssov1 6058 nnmord 6496 findcard2 6867 findcard2s 6868 addn0nid 8293 nn0n0n1ge2 9282 xnegdi 9825 efne0 11641 divgcdcoprmex 12056 pceulem 12248 pcqmul 12257 pcqcl 12260 pcaddlem 12292 pcadd 12293 grpinvnz 12770 |
Copyright terms: Public domain | W3C validator |