Metamath Proof Explorer


Theorem mprgbir

Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004)

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

Proof

Step Hyp Ref Expression
1 mprgbir.1 φxAψ
2 mprgbir.2 xAψ
3 2 rgen xAψ
4 3 1 mpbir φ