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 181 pm2.18da 798 oplem1 1051 axc11n 2444 weniso 7101 infssuni 8809 ordtypelem10 8985 oismo 8998 rankval3b 9249 grur1 10236 sqeqd 14519 hausflimi 22582 minveclem4 24029 ovolunnul 24095 vitali 24208 itg2mono 24348 frgrncvvdeqlem8 28079 minvecolem4 28651 contrd 35369 fppr2odd 43890 |
Copyright terms: Public domain | W3C validator |