Theorem mpidan

A deduction which "stacks" a hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.)

Hypotheses
mpidan.1
\( \vdash \varphi \rightarrow \chi \)
mpidan.2
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
Proof
mpidan.1
l1
adantr _
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
mpidan.2
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
mpdan l1 _