![]() |
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 180 | 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 195 pm2.01da 797 swopo 5597 onssneli 6484 oalimcl 8582 rankcf 10811 prlem934 11067 supsrlem 11145 rpnnen1lem5 13011 rennim 15239 smu01lem 16480 opsrtoslem2 22065 cfinufil 23920 alexsub 24037 ostth3 27664 4cyclusnfrgr 30222 cvnref 32221 pconnconn 35072 untelirr 35543 dfon2lem4 35623 heiborlem10 37534 lindslinindsimp1 47876 |
Copyright terms: Public domain | W3C validator |