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 121 | . 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 124 pm2.61d 169 pm2.18da 458 oplem1 999 axc11n 2295 axc11nOLD 2296 axc11nOLDOLD 2297 axc11nALT 2298 weniso 6504 infssuni 8140 ordtypelem10 8315 oismo 8328 rankval3b 8572 grur1 9521 sqeqd 13754 hausflimi 21594 minveclem4 23011 ovolunnul 23075 vitali 23188 itg2mono 23326 pilem3 24011 frgrancvvdeqlemB 26565 minvecolem4 27120 contrd 33069 frgrncvvdeqlemB 41477 |
Copyright terms: Public domain | W3C validator |