Theorem mprg 1700

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 1698	. 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 958  A.wral 1645

This theorem is referenced by:  r19.22i 1732  iuneq2i 2580  iineq2i 2581  dfiun2 2587  reuxfr2 2903  elrnopab 3801  elrnoprab 4125  rankuni2 4690  rankval4 4702  unidom 4808  sumeq2i 6988  fsump1 7006  infcvglem1 7221  infcvglem2 7222  expcnvlem1 7227  subtop 7646  projlem17 9202  goeq 10200

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

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

Copyright terms: Public domain