Theorem
mpd3an3
An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
Hypotheses
mpd3an3.2
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
mpd3an3.3
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
Proof
l0
mpd3an3.2
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
mpd3an3.3
3expa
_
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
mpdan
l0
_
This is the content in the right pane.