|   | 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.) 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 2430 weniso 7375 infssuni 9387 ordtypelem10 9568 oismo 9581 rankval3b 9867 grur1 10861 sqeqd 15206 hausflimi 23989 minveclem4 25467 ovolunnul 25536 vitali 25649 itg2mono 25789 frgrncvvdeqlem8 30326 minvecolem4 30900 contrd 38105 fppr2odd 47723 | 
| Copyright terms: Public domain | W3C validator |