Metamath Proof Explorer

Theorem anim2d

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993)

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

Proof

Step Hyp Ref Expression
1 anim1d.1 
 |-  ( ph -> ( ps -> ch ) )
2 idd 
 |-  ( ph -> ( th -> th ) )
3 2 1 anim12d 
 |-  ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )