Metamath Proof Explorer

Theorem imp

Description: Importation inference. (Contributed by NM, 3-Jan-1993) (Proof shortened by Eric Schmidt, 22-Dec-2006)

Ref Expression
Hypothesis imp.1 
|- ( ph -> ( ps -> ch ) )
Assertion imp 
|- ( ( ph /\ ps ) -> ch )

Proof

Step Hyp Ref Expression
1 imp.1 
 |-  ( ph -> ( ps -> ch ) )
2 df-an 
 |-  ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) )
3 1 impi 
 |-  ( -. ( ph -> -. ps ) -> ch )
4 2 3 sylbi 
 |-  ( ( ph /\ ps ) -> ch )