| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > necon2ad | Unicode version | ||
| Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.) |
| Ref | Expression |
|---|---|
| necon2ad.1 |
|
| Ref | Expression |
|---|---|
| necon2ad |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | necon2ad.1 |
. . 3
| |
| 2 | 1 | con2d 625 |
. 2
|
| 3 | df-ne 2376 |
. 2
| |
| 4 | 2, 3 | imbitrrdi 162 |
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 615 ax-in2 616 |
| This theorem depends on definitions: df-bi 117 df-ne 2376 |
| This theorem is referenced by: necon2d 2434 prneimg 3814 tz7.2 4400 nordeq 4591 pr2ne 7299 ltne 8156 apne 8695 xrltne 9934 npnflt 9936 nmnfgt 9939 ge0nemnf 9945 rpexp 12417 sqrt2irr 12426 pcgcd1 12593 nzrunit 13892 lgsmod 15445 |
| Copyright terms: Public domain | W3C validator |