![]() |
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 128. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) Revised to shorten pm2.18 128. (Revised by Wolf Lammen, 17-Nov-2023.) |
Ref | Expression |
---|---|
pm2.18d.1 | ⊢ (𝜑 → (¬ 𝜓 → 𝜓)) |
Ref | Expression |
---|---|
pm2.18d | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
2 | pm2.18d.1 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝜓)) | |
3 | pm2.21 123 | . . 3 ⊢ (¬ 𝜓 → (𝜓 → ¬ 𝜑)) | |
4 | 2, 3 | sylcom 30 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜑)) |
5 | 1, 4 | mt4d 117 | 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.18 128 pm2.61d 179 pm2.18da 799 oplem1 1056 axc11n 2426 weniso 7351 infssuni 9343 ordtypelem10 9522 oismo 9535 rankval3b 9821 grur1 10815 sqeqd 15113 hausflimi 23484 minveclem4 24949 ovolunnul 25017 vitali 25130 itg2mono 25271 frgrncvvdeqlem8 29559 minvecolem4 30133 contrd 36965 fppr2odd 46399 |
Copyright terms: Public domain | W3C validator |