Metamath Proof Explorer

Theorem ancl

Description: Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994)

Ref Expression
Assertion ancl 
|- ( ( ph -> ps ) -> ( ph -> ( ph /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 pm3.2 
 |-  ( ph -> ( ps -> ( ph /\ ps ) ) )
2 1 a2i 
 |-  ( ( ph -> ps ) -> ( ph -> ( ph /\ ps ) ) )