![]() |
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 2792 elndif 3127 ssddif 3236 unssdif 3237 n0i 3294 preleq 4386 dcextest 4411 dmsn0el 4915 funtpg 5080 ftpg 5497 acexmidlemab 5662 reldmtpos 6034 nntri2 6271 nntri3 6274 nndceq 6276 inffiexmid 6678 elni2 6936 renfdisj 7609 fzdisj 9529 isumrblem 10828 |
Copyright terms: Public domain | W3C validator |