![]() |
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 798 swopo 5561 onssneli 6438 oalimcl 8512 rankcf 10720 prlem934 10976 supsrlem 11054 rpnnen1lem5 12913 rennim 15131 smu01lem 16372 opsrtoslem2 21479 cfinufil 23295 alexsub 23412 ostth3 27002 4cyclusnfrgr 29278 cvnref 31275 pconnconn 33865 untelirr 34319 dfon2lem4 34400 heiborlem10 36308 lindslinindsimp1 46612 |
Copyright terms: Public domain | W3C validator |