Metamath Proof Explorer

Theorem adantr

Description: Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993)

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

Proof

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