Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm2.01d | Structured version Visualization version GIF version |
Description: Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.) |
Ref | Expression |
---|---|
pm2.01d.1 | ⊢ (𝜑 → (𝜓 → ¬ 𝜓)) |
Ref | Expression |
---|---|
pm2.01d | ⊢ (𝜑 → ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.01d.1 | . 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓)) | |
2 | id 22 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜓) | |
3 | 1, 2 | pm2.61d1 170 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: pm2.65d 186 pm2.01da 457 swopo 4969 onssneli 5754 oalimcl 7527 rankcf 9478 prlem934 9734 supsrlem 9811 rpnnen1lem5 11694 rpnnen1lem5OLD 11700 rennim 13827 smu01lem 15045 opsrtoslem2 19306 cfinufil 21542 alexsub 21659 ostth3 25127 4cyclusnfrgra 26546 cvnref 28534 pconcon 30467 untelirr 30839 dfon2lem4 30935 heiborlem10 32789 4cyclusnfrgr 41462 lindslinindsimp1 42040 |
Copyright terms: Public domain | W3C validator |