Metamath Proof Explorer

Theorem expt

Description: Exportation theorem pm3.3 (closed form of ex ) expressed with primitive connectives. (Contributed by NM, 28-Dec-1992)

Ref Expression
Assertion expt 
|- ( ( -. ( ph -> -. ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )

Proof

Step Hyp Ref Expression
1 pm3.2im 
 |-  ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2 1 imim1d 
 |-  ( ph -> ( ( -. ( ph -> -. ps ) -> ch ) -> ( ps -> ch ) ) )
3 2 com12 
 |-  ( ( -. ( ph -> -. ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )