Metamath Proof Explorer

Theorem adantrd

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994)

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

Proof

Step Hyp Ref Expression
1 adantrd.1 
 |-  ( ph -> ( ps -> ch ) )
2 simpl 
 |-  ( ( ps /\ th ) -> ps )
3 2 1 syl5 
 |-  ( ph -> ( ( ps /\ th ) -> ch ) )