![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon2bd | Structured version Visualization version Unicode version |
Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.) |
Ref | Expression |
---|---|
necon2bd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
necon2bd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon2bd.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-ne 2623 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6ib 230 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con2d 119 |
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 189 df-ne 2623 |
This theorem is referenced by: necon4bd 2643 necon4d 2647 disjiun 4392 eceqoveq 7465 en3lp 8118 infpssrlem5 8734 nneo 11016 zeo2 11019 sqrt2irr 14294 coprm 14650 dfphi2 14715 pltirr 16202 oddvdsnn0 17186 psgnodpmr 19151 supnfcls 21028 flimfnfcls 21036 metds0 21860 metdseq0 21864 metnrmlem1a 21868 metds0OLD 21875 metdseq0OLD 21879 metnrmlem1aOLD 21883 sineq0 23469 lgsqr 24267 staddi 27892 stadd3i 27894 eulerpartlems 29186 erdszelem8 29914 finminlem 30967 ordcmp 31100 poimirlem18 31951 poimirlem21 31954 cvrnrefN 32842 trlnidatb 33737 bezoutr1 35830 |
Copyright terms: Public domain | W3C validator |