This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mprg

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

Ref Expression
Hypotheses mprg.1 ⊢ ∀ x ∈ A φ → ψ
mprg.2 ⊢ x ∈ A → φ
Assertion mprg ⊢ ψ

Proof

Step Hyp Ref Expression
1 mprg.1 ⊢ ∀ x ∈ A φ → ψ
2 mprg.2 ⊢ x ∈ A → φ
3 2 rgen ⊢ ∀ x ∈ A φ
4 3 1 ax-mp ⊢ ψ