Metamath Proof Explorer


Theorem ad2ant2rl

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007)

Ref Expression
Hypothesis ad2ant2.1 φψχ
Assertion ad2ant2rl φθτψχ

Proof

Step Hyp Ref Expression
1 ad2ant2.1 φψχ
2 1 adantrl φτψχ
3 2 adantlr φθτψχ