Theorem mpg 684

Description: Modus ponens combined with generalization.

Hypotheses

Ref	Expression
mpg.1	⊢ (∀xφ → ψ)
mpg.2	⊢ φ

Assertion

Ref	Expression
mpg	⊢ ψ

Proof of Theorem mpg

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

Syntax hints:   → wi 2  ∀wal 672

This theorem is referenced by:  mpgbi 685  mpgbir 686  a5i 687  bial 695  19.22i 723  biex 733  ax9a 808  cbv3 847  cbval 848  chv2 850  sbt 899  sbeq1 900  sbeq2 901  chv 984  moan 1046  moor 1048  2moex 1060  2eumo 1062  2exeu 1066  2eu1 1067  vtoclf 1377  vtocl2 1379  vtocl3 1380  euxfr2 1435  dtrucor 1890  caoprmo 3084  th3qlem2 3251  tz9.13 3507  axpowndlem3 3745  infxpidmlem9 4941

This theorem was proved from axioms:  ax-mp 6  ax-gen 677

metamath.org