Metamath Proof Explorer

Theorem impi

Description: An importation inference. (Contributed by NM, 29-Dec-1992) (Proof shortened by Wolf Lammen, 20-Jul-2013)

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

Proof

Step Hyp Ref Expression
1 impi.1 
 |-  ( ph -> ( ps -> ch ) )
2 1 con3rr3 
 |-  ( -. ch -> ( ph -> -. ps ) )
3 2 con1i 
 |-  ( -. ( ph -> -. ps ) -> ch )