Theorem mpg 1427

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

Hypotheses

Ref	Expression
mpg.1	⊢ (∀𝑥𝜑 → 𝜓)
mpg.2	⊢ 𝜑

Assertion

Ref	Expression
mpg	⊢ 𝜓

Proof of Theorem mpg

Step	Hyp	Ref	Expression
1		mpg.2	. . 3 ⊢ 𝜑
2	1	ax-gen 1425	. 2 ⊢ ∀𝑥𝜑
3		mpg.1	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
4	2, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4  ∀wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-gen 1425

This theorem is referenced by:  alimi  1431  albii  1446  a5i  1522  eximi  1579  exbii  1584  19.9h  1622  hbn  1632  chvar  1730  equsb1  1758  equsb2  1759  chvarvv  1880  chvarv  1909  moimi  2064  2eumo  2087  vtoclf  2739  vtocl2  2741  vtocl3  2742  spcimgf  2766  spcimegf  2767  spcgf  2768  spcegf  2769  mosub  2862  csbexa  4057  nalset  4058  ssopab2i  4199  pwnex  4370  eusv2nf  4377  iotabii  5110  fvmptss2  5496  eufnfv  5648  riotaexg  5734  xpcomco  6720  bj-ex  12969  ch2var  12974  bj-vtoclgf  12983  elabgf1  12986  bj-rspg  12994  sumdc2  13006  bdsepnf  13086  bj-nalset  13093  setindf  13164  strcollnf  13183