Theorem
mp2and
A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
mp2and.1
\( \vdash \varphi \rightarrow \psi \)
mp2and.2
\( \vdash \varphi \rightarrow \chi \)
mp2and.3
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
mp2and.2
\( \vdash \varphi \rightarrow \chi \)
l1
mp2and.1
\( \vdash \varphi \rightarrow \psi \)
mp2and.3
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \theta \)
mpand
l1
_
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
mpd
l0
_
This is the content in the right pane.