![]() |
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 626 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 614 ax-in2 615 |
This theorem is referenced by: nsyl 628 notnot 629 imanim 688 imnan 690 pm4.53r 751 ioran 752 pm3.1 754 oranim 781 xornbi 1386 exalim 1502 exnalim 1646 festino 2132 calemes 2142 fresison 2144 calemos 2145 fesapo 2146 nner 2351 necon2ai 2401 necon2bi 2402 neneqad 2426 ralexim 2469 rexalim 2470 eueq3dc 2913 elndif 3261 ssddif 3371 unssdif 3372 n0i 3430 preleq 4556 dcextest 4582 dmsn0el 5100 funtpg 5269 ftpg 5703 acexmidlemab 5872 reldmtpos 6257 nntri2 6498 nntri3 6501 nndceq 6503 inffiexmid 6909 ctssdccl 7113 mkvprop 7159 elni2 7316 renfdisj 8020 sup3exmid 8917 fzdisj 10055 sumrbdclem 11388 prodrbdclem 11582 lgsval2lem 14551 |
Copyright terms: Public domain | W3C validator |