Description: Importation theorem pm3.1 (closed form of imp ) expressed with primitive connectives. (Contributed by NM, 25-Apr-1994) (Proof shortened by Wolf Lammen, 20-Jul-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | impt | |- ( ( ph -> ( ps -> ch ) ) -> ( -. ( ph -> -. ps ) -> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simprim | |- ( -. ( ph -> -. ps ) -> ps ) |
|
| 2 | simplim | |- ( -. ( ph -> -. ps ) -> ph ) |
|
| 3 | 2 | imim1i | |- ( ( ph -> ( ps -> ch ) ) -> ( -. ( ph -> -. ps ) -> ( ps -> ch ) ) ) |
| 4 | 1 3 | mpdi | |- ( ( ph -> ( ps -> ch ) ) -> ( -. ( ph -> -. ps ) -> ch ) ) |