Theorem mpg 984

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 961	. 2 ⊢ ∀xφ
3		mpg.1	. 2 ⊢ (∀xφ → ψ)
4	2, 3	ax-mp 7	1 ⊢ ψ

Syntax hints:   → wi 3  ∀wal 952

This theorem is referenced by:  mpgbi 985  mpgbir 986  a5i 987  albii 997  hbn 1002  19.9 1034  19.22i 1038  exbii 1049  ax9 1122  cbv3 1162  cbval 1163  chvar 1165  sbt 1190  equsb1 1191  equsb2 1192  chvarv 1325  immoi 1416  2eumo 1440  vtoclf 1837  vtocl2 1839  vtocl3 1840  euxfr2 1922  axsep 2697  axnul2 2703  dtrucor 2768  tz9.13 4643  ac7 4728  axpowndlem3 4931  infxpidmlem9 7511

This theorem was proved from axioms:  ax-mp 7  ax-gen 961

Copyright terms: Public domain