![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > con3i | GIF version |
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.) |
Ref | Expression |
---|---|
con3i.a | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
con3i | ⊢ (¬ 𝜓 → ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜓) | |
2 | con3i.a | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | nsyl 629 | 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 615 ax-in2 616 |
This theorem is referenced by: notnotnot 635 conax1 654 pm5.21ni 704 pm2.45 739 pm2.46 740 pm3.14 754 3ianorr 1319 nalequcoms 1527 equidqe 1542 nnal 1659 ax6blem 1660 hbnt 1663 naecoms 1734 euor2 2094 moexexdc 2120 baroco 2143 necon3ai 2406 necon3bi 2407 nnral 2477 eueq3dc 2923 difin 3384 indifdir 3403 difrab 3421 csbprc 3480 ifandc 3584 nelpri 3628 nelprd 3630 opprc 3811 opprc1 3812 opprc2 3813 notnotsnex 4199 eldifpw 4489 nlimsucg 4577 nfvres 5560 nfunsn 5561 ressnop0 5710 ovprc 5923 ovprc1 5924 ovprc2 5925 mapprc 6666 ixpprc 6733 ixp0 6745 fiprc 6829 fidceq 6883 unfiexmid 6931 difinfsnlem 7112 3nsssucpw1 7249 onntri51 7253 onntri52 7257 fzdcel 10054 bcpasc 10760 flodddiv4lt 11955 bj-nnan 14784 bj-imnimnn 14786 nnnotnotr 15038 nninfsellemsuc 15058 |
Copyright terms: Public domain | W3C validator |