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 )