Theorem mprgbir 1704

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 1701	. 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 960  A.wral 1648

This theorem is referenced by:  ss2rabi 2131  ssintub 2555  po0 2855  so0 2871  ordon 2993  onxpdisj 3247  tfrlem6 3922  oawordeulem 4194  sbthlem1 4453  rankuni2 4700  rankval4 4712  ac6lem 4764  ioomax 6394  climsup 7155  serzf0 7169  ser1f0 7170  ser1clim0 7173  iincld 7676  neiint 7716  neips 7724  cncnplem4 7774  ubthlem5 8529  sincolem 8660  shintcl 9288  bra11 10036  idleop 10059  cayleylem3 10406  inposet 10477  fgsb 10555  fgsb2 10560  rcfpfil 10569

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

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

Copyright terms: Public domain