Theorem 3adant1r

Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Hypothesis
ad4ant3.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \tau \wedge \psi \wedge \chi \rightarrow \theta \)
Proof
l0
simpl
\( \vdash \varphi \wedge \tau \rightarrow \varphi \)
ad4ant3.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
syl3an1 l0 _