Theorem mprgbir 2927

Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)

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

Syntax hints:   -> wi 4   <-> wb 196   e. wcel 1990   A.wral 2912

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

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  ss2rabi  3684  rabxm  3961  ssintub  4495  djussxp  5267  dmiin  5369  dfco2  5634  coiun  5645  tron  5746  onxpdisj  5847  wfrrel  7420  wfrdmss  7421  tfrlem6  7478  oawordeulem  7634  sbthlem1  8070  marypha2lem1  8341  rankval4  8730  tcwf  8746  fin23lem16  9157  fin23lem29  9163  fin23lem30  9164  itunitc  9243  acncc  9262  wfgru  9638  renfdisj  10098  ioomax  12248  iccmax  12249  hashgval2  13167  fsumcom2  14505  fsumcom2OLD  14506  fprodcom2  14714  fprodcom2OLD  14715  dfphi2  15479  dmcoass  16716  letsr  17227  efgsf  18142  lssuni  18940  lpival  19245  psr1baslem  19555  cnsubdrglem  19797  retos  19964  istopon  20717  neips  20917  filssufilg  21715  xrhmeo  22745  iscmet3i  23110  ehlbase  23194  ovolge0  23249  unidmvol  23309  resinf1o  24282  divlogrlim  24381  dvloglem  24394  logf1o2  24396  atansssdm  24660  ppiub  24929  sspval  27578  shintcli  28188  lnopco0i  28863  imaelshi  28917  nmopadjlem  28948  nmoptrii  28953  nmopcoi  28954  nmopcoadji  28960  idleop  28990  hmopidmchi  29010  hmopidmpji  29011  xrsclat  29680  rearchi  29842  dmvlsiga  30192  sxbrsigalem0  30333  dya2iocucvr  30346  eulerpartlemgh  30440  bnj110  30928  subfacp1lem1  31161  erdszelem2  31174  dfon2lem3  31690  trpredlem1  31727  frrlem6  31789  frrlem7  31790  filnetlem2  32374  taupi  33169  cnviun  37942  coiun1  37944  comptiunov2i  37998  cotrcltrcl  38017  cotrclrcl  38034  ssrab2f  39300  iooinlbub  39723  stirlinglem14  40304  sssalgen  40553