Metamath Proof Explorer


Theorem ad2antrr

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999) (Proof shortened by Wolf Lammen, 20-Nov-2012)

Ref Expression
Hypothesis ad2ant.1 ( 𝜑𝜓 )
Assertion ad2antrr ( ( ( 𝜑𝜒 ) ∧ 𝜃 ) → 𝜓 )

Proof

Step Hyp Ref Expression
1 ad2ant.1 ( 𝜑𝜓 )
2 1 adantr ( ( 𝜑𝜃 ) → 𝜓 )
3 2 adantlr ( ( ( 𝜑𝜒 ) ∧ 𝜃 ) → 𝜓 )