![]() |
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 181 | 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 197 pm2.01da 795 swopo 5372 onssneli 6175 oalimcl 8036 rankcf 10045 prlem934 10301 supsrlem 10379 rpnnen1lem5 12230 rennim 14432 smu01lem 15667 opsrtoslem2 19952 cfinufil 22220 alexsub 22337 ostth3 25896 4cyclusnfrgr 27763 cvnref 29759 pconnconn 32086 untelirr 32542 dfon2lem4 32639 heiborlem10 34630 lindslinindsimp1 43992 |
Copyright terms: Public domain | W3C validator |