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 ) )