Theorem mpdan

An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses
mpdan.1
\( \vdash \varphi \rightarrow \psi \)
mpdan.2
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
id
\( \vdash \varphi \rightarrow \varphi \)
l1
mpdan.1
\( \vdash \varphi \rightarrow \psi \)
mpdan.2
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
syl2anc l0 l1 _