![]() |
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 5555 onssneli 6431 oalimcl 8500 rankcf 10672 prlem934 10928 supsrlem 11006 rpnnen1lem5 12861 rennim 15084 smu01lem 16325 opsrtoslem2 21415 cfinufil 23231 alexsub 23348 ostth3 26938 4cyclusnfrgr 29065 cvnref 31062 pconnconn 33629 untelirr 34085 dfon2lem4 34171 heiborlem10 36211 lindslinindsimp1 46433 |
Copyright terms: Public domain | W3C validator |