![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con1bii | Structured version Visualization version Unicode version |
Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.) |
Ref | Expression |
---|---|
con1bii.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
con1bii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot 293 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | con1bii.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | xchbinx 312 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | bicomi 206 |
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 |
This theorem is referenced by: con2bii 334 xor 902 3oran 1004 2nexaln 1702 nnel 2733 npss 3543 symdifass 3672 dfnul3 3734 snprc 4035 dffv2 5938 kmlem3 8582 axpowndlem3 9024 nnunb 10865 rpnnen2 14278 dsmmacl 19304 ntreq0 20093 largei 27920 spc2d 28107 ballotlem2 29321 dffr5 30393 brsset 30656 brtxpsd 30661 dfrecs2 30717 dfint3 30719 con1bii2 31734 notbinot1 32312 elpadd0 33374 pm10.252 36710 pm10.253 36711 2exanali 36737 |
Copyright terms: Public domain | W3C validator |