![]() |
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 1055 axc11n 2421 weniso 7356 infssuni 9361 ordtypelem10 9544 oismo 9557 rankval3b 9843 grur1 10837 sqeqd 15139 hausflimi 23877 minveclem4 25353 ovolunnul 25422 vitali 25535 itg2mono 25676 frgrncvvdeqlem8 30109 minvecolem4 30683 contrd 37564 fppr2odd 47065 |
Copyright terms: Public domain | W3C validator |