![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon2bi | Structured version Visualization version Unicode version |
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.) |
Ref | Expression |
---|---|
necon2bi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
necon2bi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon2bi.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | neneqd 2639 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | con2i 125 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 190 df-ne 2634 |
This theorem is referenced by: minel 3831 rzal 3882 difsnb 4126 dtrucor2 4647 kmlem6 8610 winainflem 9143 0npi 9332 0npr 9442 0nsr 9528 1div0 10298 rexmul 11585 rennim 13350 mrissmrcd 15594 prmirred 19114 pthaus 20701 rplogsumlem2 24371 pntrlog2bndlem4 24466 pntrlog2bndlem5 24467 1div0apr 25953 bnj1311 29881 subfacp1lem6 29956 bj-dtrucor2v 31460 itg2addnclem3 32039 cdleme31id 34005 sdrgacs 36111 rzalf 37377 jumpncnp 37813 fourierswlem 38131 |
Copyright terms: Public domain | W3C validator |