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 558 | 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 544 ax-in2 545 |
This theorem is referenced by: pm2.51 581 pm5.21ni 619 notnotnot 628 pm2.45 657 pm2.46 658 pm3.14 670 3ianorr 1204 nalequcoms 1410 equidqe 1425 ax6blem 1540 hbnt 1543 naecoms 1612 euor2 1958 moexexdc 1984 baroco 2007 necon3ai 2254 necon3bi 2255 eueq3dc 2715 difin 3174 indifdir 3193 difrab 3211 csbprc 3262 nelpri 3399 opprc 3570 opprc1 3571 opprc2 3572 eldifpw 4208 nlimsucg 4290 nfvres 5206 nfunsn 5207 ressnop0 5344 ovprc 5540 ovprc1 5541 ovprc2 5542 fiprc 6292 fidceq 6330 fzdcel 8904 |
Copyright terms: Public domain | W3C validator |