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 797 oplem1 1054 axc11n 2424 weniso 7281 infssuni 9208 ordtypelem10 9384 oismo 9397 rankval3b 9683 grur1 10677 sqeqd 14976 hausflimi 23237 minveclem4 24702 ovolunnul 24770 vitali 24883 itg2mono 25024 frgrncvvdeqlem8 28958 minvecolem4 29530 contrd 36360 fppr2odd 45534 |
Copyright terms: Public domain | W3C validator |