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 600 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 588 ax-in2 589 |
This theorem is referenced by: nsyl 602 notnot 603 imanim 662 imnan 664 pm4.53r 725 ioran 726 pm3.1 728 oranim 755 xornbi 1349 exalim 1463 exnalim 1610 festino 2083 calemes 2093 fresison 2095 calemos 2096 fesapo 2097 nner 2289 necon2ai 2339 necon2bi 2340 neneqad 2364 ralexim 2406 rexalim 2407 eueq3dc 2831 elndif 3170 ssddif 3280 unssdif 3281 n0i 3338 preleq 4440 dcextest 4465 dmsn0el 4978 funtpg 5144 ftpg 5572 acexmidlemab 5736 reldmtpos 6118 nntri2 6358 nntri3 6361 nndceq 6363 inffiexmid 6768 ctssdccl 6964 mkvprop 7000 elni2 7090 renfdisj 7792 sup3exmid 8683 fzdisj 9800 sumrbdclem 11113 |
Copyright terms: Public domain | W3C validator |