Metamath Proof Explorer

Theorem impac

Description: Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994)

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

Proof

Step Hyp Ref Expression
1 impac.1 
 |-  ( ph -> ( ps -> ch ) )
2 1 ancrd 
 |-  ( ph -> ( ps -> ( ch /\ ps ) ) )
3 2 imp 
 |-  ( ( ph /\ ps ) -> ( ch /\ ps ) )