Theorem mprg 1692

Description: Modus ponens combined with restricted generalization.

Hypotheses

Ref	Expression
mprg.1	|- (A.x e. A ph -> ps)
mprg.2	|- (x e. A -> ph)

Assertion

Ref	Expression
mprg	|- ps

Proof of Theorem mprg

Step	Hyp	Ref	Expression
1		mprg.2	. . 3 |- (x e. A -> ph)
2	1	rgen 1690	. 2 |- A.x e. A ph
3		mprg.1	. 2 |- (A.x e. A ph -> ps)
4	2, 3	ax-mp 7	1 |- ps

Syntax hints:   -> wi 3   e. wcel 955  A.wral 1637

This theorem is referenced by:  r19.22i 1724  iuneq2i 2570  iineq2i 2571  dfiun2 2577  reuxfr2 2893  elrnopab 3786  elrnoprab 4109  rankuni2 4662  rankval4 4674  unidom 4780  sumeq2i 6926  fsump1 6944  infcvglem1 7156  infcvglem2 7157  expcnvlem1 7162  subtop 7588  projlem17 9118  goeq 10110

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960

This theorem depends on definitions:  df-bi 147  df-ral 1641

Copyright terms: Public domain