![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.18d | Structured version Visualization version GIF version |
Description: Deduction form of the Clavius law pm2.18 125. (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 125 | . 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: pm2.61d 172 pm2.18da 790 oplem1 1040 axc11n 2392 weniso 6876 infssuni 8545 ordtypelem10 8721 oismo 8734 rankval3b 8986 grur1 9977 sqeqd 14313 hausflimi 22192 minveclem4 23638 ovolunnul 23704 vitali 23817 itg2mono 23957 pilem3OLD 24645 frgrncvvdeqlem8 27714 minvecolem4 28308 contrd 34522 |
Copyright terms: Public domain | W3C validator |