![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.18d | Structured version Visualization version GIF version |
Description: Deduction based on reductio ad absurdum. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
pm2.18d.1 | ⊢ (𝜑 → (¬ 𝜓 → 𝜓)) |
Ref | Expression |
---|---|
pm2.18d | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.18d.1 | . 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜓)) | |
2 | pm2.18 122 | . 2 ⊢ ((¬ 𝜓 → 𝜓) → 𝜓) | |
3 | 1, 2 | syl 17 | 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: notnotr 125 pm2.61d 170 pm2.18da 458 oplem1 1027 axc11n 2342 axc11nOLD 2343 weniso 6644 infssuni 8298 ordtypelem10 8473 oismo 8486 rankval3b 8727 grur1 9680 sqeqd 13950 hausflimi 21831 minveclem4 23249 ovolunnul 23314 vitali 23427 itg2mono 23565 pilem3 24252 frgrncvvdeqlem8 27286 minvecolem4 27864 contrd 34029 |
Copyright terms: Public domain | W3C validator |