Description: A nested modus ponens inference. Inference associated with com12 . (Contributed by NM, 29-Dec-1992) (Proof shortened by Stefan Allan, 20-Mar-2006)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mpi.1 | |- ps |
|
| mpi.2 | |- ( ph -> ( ps -> ch ) ) |
||
| Assertion | mpi | |- ( ph -> ch ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpi.1 | |- ps |
|
| 2 | mpi.2 | |- ( ph -> ( ps -> ch ) ) |
|
| 3 | 1 | a1i | |- ( ph -> ps ) |
| 4 | 3 2 | mpd | |- ( ph -> ch ) |