Theorem mprgbir 1701

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 1698	. 2 |- A.x e. A ps
3		mprgbir.1	. 2 |- (ph <-> A.x e. A ps)
4	2, 3	mpbir 190	1 |- ph

Syntax hints:   -> wi 3   <-> wb 146   e. wcel 958  A.wral 1645

This theorem is referenced by:  ss2rabi 2128  ssintub 2551  po0 2849  so0 2865  ordon 2987  onxpdisj 3241  tfrlem6 3916  oawordeulem 4188  sbthlem1 4447  rankuni2 4690  rankval4 4702  ac6lem 4754  ioomax 6393  climsup 7155  serzf0 7169  ser1f0 7170  ser1clim0 7173  iincld 7679  neiint 7719  neips 7727  cncnplem4 7777  ubthlem5 8533  sincolem 8665  shintcl 9293  bra11 10041  idleop 10064  cayleylem3 10411  fgsb 10570  fgsbOLD 10571  fgsb2 10580  rcfpfil 10597  rcfpfilOLD 10598

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