Theorem mprgbir 1693

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 1690	. 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 955  A.wral 1637

This theorem is referenced by:  ss2rabi 2118  ssintub 2541  po0 2840  so0 2856  ordon 2977  onxpdisj 3231  tfrlem6 3901  oawordeulem 4172  sbthlem1 4427  rankuni2 4662  rankval4 4674  ac6lem 4726  ioomax 6325  climsup 7091  serzf0 7105  ser1f0 7106  ser1clim0 7109  iincld 7621  neiint 7660  neips 7668  cncnplem4 7716  ubthlem5 8464  sincolem 8584  shintcl 9208  bra11 9954  idleop 9976  cayleylem3 10318  fgsb 10444  fgsb2 10449

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