Theorem mprgbir 1250

Description: Modus ponens on biconditional combined with restricted generalization.

Hypotheses

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

Assertion

Ref	Expression
mprgbir	|- ph

Proof of Theorem mprgbir

Step	Hyp	Ref	Expression
1		mprgbir.2	. . 3 |- (x e. A -> ps)
2	1	rgen 1247	. 2 |- A.x e. A ps
3		mprgbir.1	. 2 |- (ph <-> A.x e. A ps)
4	2, 3	mpbir 165	1 |- ph

Syntax hints:   -> wi 2   <-> wb 127   e. wcel 1092  A.wral 1201

This theorem is referenced by:  ss2rabi 1554  ssintub 1981  po0 2137  so0 2153  ordon 2238  onxpdisj 2476  tfrlem6 2954  oawordeulem 3156  sbthlem1 3349  rankuni 3533  rankuniss 3534  ranklon 3540  ac6lem 3575  shintcl 5294

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

This theorem depends on definitions:  df-bi 128  df-ral 1205

metamath.org