Theorem anmp

Modus ponens for { \/ , -. } axiom systems. (Contributed by Anthony Hart, 12-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
anmp.min
\( \vdash \varphi \)
anmp.maj
\( \vdash \neg \varphi \vee \psi \)
Conclusion
\( \vdash \psi \)
Proof
l0
anmp.min
\( \vdash \varphi \)
anmp.maj
imorri _
\( \vdash \varphi \rightarrow \psi \)
ax-mp l0 _