Theorem mpg 1356

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 1354	. 2 ⊢ ∀𝑥𝜑
3		mpg.1	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
4	2, 3	ax-mp 7	1 ⊢ 𝜓

Syntax hints:   → wi 4  ∀wal 1257

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

This theorem is referenced by:  alimi  1360  albii  1375  a5i  1451  eximi  1507  exbii  1512  19.9h  1550  hbn  1560  chvar  1656  equsb1  1684  equsb2  1685  chvarv  1828  moimi  1981  2eumo  2004  vtoclf  2624  vtocl2  2626  vtocl3  2627  spcimgf  2650  spcimegf  2651  spcgf  2652  spcegf  2653  mosub  2741  csbexa  3913  nalset  3914  ssopab2i  4041  eusv2nf  4215  iotabii  4916  fvmptss2  5274  eufnfv  5416  riotaexg  5499  xpcomco  6330  bj-ex  10261  ch2var  10266  bj-vtoclgf  10274  elabgf1  10277  bj-rspg  10285  bdsepnf  10367  bj-nalset  10374  setindf  10450  strcollnf  10469