Theorem mpg

Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.)

Hypotheses
mpg.1
\( \vdash \forall x \, \varphi \rightarrow \psi \)
mpg.2
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \)
Proof
mpg.2
l1
ax-gen _
\( \vdash \forall x \, \varphi \)
mpg.1
\( \vdash \forall x \, \varphi \rightarrow \psi \)
ax-mp l1 _