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

Metamath Proof Explorer

Theorem mpg

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

Ref Expression
Hypotheses mpg.1 ⊢ ∀ x φ → ψ
mpg.2 ⊢ φ
Assertion mpg ⊢ ψ

Proof

Step Hyp Ref Expression
1 mpg.1 ⊢ ∀ x φ → ψ
2 mpg.2 ⊢ φ
3 2 ax-gen ⊢ ∀ x φ
4 3 1 ax-mp ⊢ ψ