Metamath Proof Explorer

Theorem expi

Description: An exportation inference. (Contributed by NM, 29-Dec-1992) (Proof shortened by Mel L. O'Cat, 28-Nov-2008)

Ref Expression
Hypothesis expi.1 
|- ( -. ( ph -> -. ps ) -> ch )
Assertion expi 
|- ( ph -> ( ps -> ch ) )

Proof

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