Theorem re1axmp

[ax-mp] derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
re1axmp.min
\( \vdash \varphi \)
re1axmp.maj
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \psi \)
Proof
l0
re1axmp.min
\( \vdash \varphi \)
l1
re1axmp.maj
\( \vdash \varphi \rightarrow \psi \)
rb-imdf
rblem6 _
\( \vdash \neg (\varphi \rightarrow \psi) \vee (\neg \varphi \vee \psi) \)
anmp l1 _
\( \vdash \neg \varphi \vee \psi \)
anmp l0 _