Metamath Proof Explorer


Theorem adantrl

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994) (Proof shortened by Wolf Lammen, 24-Nov-2012)

Ref Expression
Hypothesis adant2.1 ( ( 𝜑𝜓 ) → 𝜒 )
Assertion adantrl ( ( 𝜑 ∧ ( 𝜃𝜓 ) ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 adant2.1 ( ( 𝜑𝜓 ) → 𝜒 )
2 simpr ( ( 𝜃𝜓 ) → 𝜓 )
3 2 1 sylan2 ( ( 𝜑 ∧ ( 𝜃𝜓 ) ) → 𝜒 )