![]() |
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 600 | 1 ⊢ (¬ 𝜓 → ¬ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 586 ax-in2 587 |
This theorem is referenced by: notnotnot 606 conax1 625 pm5.21ni 675 pm2.45 710 pm2.46 711 pm3.14 725 3ianorr 1270 nalequcoms 1480 equidqe 1495 ax6blem 1611 hbnt 1614 naecoms 1685 euor2 2033 moexexdc 2059 baroco 2082 necon3ai 2331 necon3bi 2332 eueq3dc 2827 difin 3279 indifdir 3298 difrab 3316 csbprc 3374 ifandc 3474 nelpri 3517 nelprd 3519 opprc 3692 opprc1 3693 opprc2 3694 notnotsnex 4071 eldifpw 4358 nlimsucg 4441 nfvres 5408 nfunsn 5409 ressnop0 5555 ovprc 5760 ovprc1 5761 ovprc2 5762 mapprc 6500 ixpprc 6567 ixp0 6579 fiprc 6663 fidceq 6716 unfiexmid 6759 difinfsnlem 6936 fzdcel 9713 bcpasc 10405 flodddiv4lt 11481 bj-nnan 12641 bj-nnal 12642 bj-nnst 12657 nninfsellemsuc 12900 |
Copyright terms: Public domain | W3C validator |