Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > con2i | GIF 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 616 | 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 604 ax-in2 605 |
This theorem is referenced by: nsyl 618 notnot 619 imanim 678 imnan 680 pm4.53r 741 ioran 742 pm3.1 744 oranim 771 xornbi 1375 exalim 1489 exnalim 1633 festino 2119 calemes 2129 fresison 2131 calemos 2132 fesapo 2133 nner 2338 necon2ai 2388 necon2bi 2389 neneqad 2413 ralexim 2456 rexalim 2457 eueq3dc 2895 elndif 3241 ssddif 3351 unssdif 3352 n0i 3409 preleq 4526 dcextest 4552 dmsn0el 5067 funtpg 5233 ftpg 5663 acexmidlemab 5830 reldmtpos 6212 nntri2 6453 nntri3 6456 nndceq 6458 inffiexmid 6863 ctssdccl 7067 mkvprop 7113 elni2 7246 renfdisj 7949 sup3exmid 8843 fzdisj 9977 sumrbdclem 11304 prodrbdclem 11498 |
Copyright terms: Public domain | W3C validator |