Theorem mp3and

A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.)

Hypotheses
mp3and.1
\( \vdash \varphi \rightarrow \psi \)
mp3and.2
\( \vdash \varphi \rightarrow \chi \)
mp3and.3
\( \vdash \varphi \rightarrow \theta \)
mp3and.4
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \tau \)
Proof
l0
mp3and.1
l1
mp3and.2
mp3and.3
l3
3jca l0 l1 _
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \)
mp3and.4
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \rightarrow \tau \)
mpd l3 _