![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > con2i | Unicode version |
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.) |
Ref | Expression |
---|---|
con2i.a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
con2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con2i.a |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | id 19 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | nsyl3 592 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 580 ax-in2 581 |
This theorem is referenced by: nsyl 594 notnot 595 imnan 660 ioran 705 pm3.1 707 imanim 824 pm4.53r 843 oranim 846 xornbi 1323 exalim 1437 exnalim 1583 festino 2055 calemes 2065 fresison 2067 calemos 2068 fesapo 2069 nner 2260 necon2ai 2310 necon2bi 2311 neneqad 2335 ralexim 2373 rexalim 2374 eueq3dc 2790 elndif 3125 ssddif 3234 unssdif 3235 n0i 3292 preleq 4384 dcextest 4409 dmsn0el 4913 funtpg 5078 ftpg 5495 acexmidlemab 5660 reldmtpos 6032 nntri2 6269 nntri3 6272 nndceq 6274 inffiexmid 6676 elni2 6934 renfdisj 7607 fzdisj 9527 isumrblem 10826 |
Copyright terms: Public domain | W3C validator |