Metamath Proof Explorer


Theorem mprg

Description: Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004)

Ref Expression
Hypotheses mprg.1 xAφψ
mprg.2 xAφ
Assertion mprg ψ

Proof

Step Hyp Ref Expression
1 mprg.1 xAφψ
2 mprg.2 xAφ
3 2 rgen xAφ
4 3 1 ax-mp ψ