Description: Deduction form of the Clavius law pm2.18 . (Contributed by FL, 12-Jul-2009) (Proof shortened by Andrew Salmon, 7-May-2011) Revised to shorten pm2.18 . (Revised by Wolf Lammen, 17-Nov-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | pm2.18d.1 | |- ( ph -> ( -. ps -> ps ) ) |
|
| Assertion | pm2.18d | |- ( ph -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.18d.1 | |- ( ph -> ( -. ps -> ps ) ) |
|
| 2 | id | |- ( ph -> ph ) |
|
| 3 | pm2.21 | |- ( -. ps -> ( ps -> -. ph ) ) |
|
| 4 | 1 3 | sylcom | |- ( ph -> ( -. ps -> -. ph ) ) |
| 5 | 2 4 | mt4d | |- ( ph -> ps ) |