Description: A modus ponens deduction. A translation of natural deduction rule -> E ( -> elimination), see natded . Deduction form of ax-mp . Inference associated with a2i . Commuted form of mpcom . (Contributed by NM, 29-Dec-1992)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mpd.1 | |- ( ph -> ps ) |
|
| mpd.2 | |- ( ph -> ( ps -> ch ) ) |
||
| Assertion | mpd | |- ( ph -> ch ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpd.1 | |- ( ph -> ps ) |
|
| 2 | mpd.2 | |- ( ph -> ( ps -> ch ) ) |
|
| 3 | 2 | a2i | |- ( ( ph -> ps ) -> ( ph -> ch ) ) |
| 4 | 1 3 | ax-mp | |- ( ph -> ch ) |