Theorem mprgbir 3059

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

Hypotheses

Ref	Expression
mprgbir.1	⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
mprgbir.2	⊢ (𝑥 ∈ 𝐴 → 𝜓)

Assertion

Ref	Expression
mprgbir	⊢ 𝜑

Proof of Theorem mprgbir

Step	Hyp	Ref	Expression
1		mprgbir.2	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝜓)
2	1	rgen 3054	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓
3		mprgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
4	2, 3	mpbir 231	1 ⊢ 𝜑

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∀wral 3052

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

This theorem depends on definitions:  df-bi 207  df-ral 3053

This theorem is referenced by:  ssintub  4909  djussxp  5796  dmiin  5904  dfco2  6205  coiun  6217  tron  6342  onxpdisj  6446  epweon  7724  frrlem6  8236  frrlem7  8237  tfrlem6  8316  oawordeulem  8484  sbthlem1  9020  marypha2lem1  9343  ttrclselem1  9641  rankval4  9786  tcwf  9802  inlresf  9833  inrresf  9835  fin23lem16  10252  fin23lem29  10258  fin23lem30  10259  itunitc  10338  acncc  10357  wfgru  10734  renfdisj  11200  ioomax  13370  iccmax  13371  hashgval2  14335  fsumcom2  15731  fprodcom2  15944  dfphi2  16739  oppccatf  17689  dmcoass  18028  letsr  18554  smndex2dnrinv  18881  efgsf  19699  lssuni  20929  lpival  21318  cnsubdrglem  21412  retos  21612  psr1baslem  22162  istopon  22891  neips  23092  filssufilg  23890  xrhmeo  24927  iscmet3i  25293  ehlbase  25396  ovolge0  25462  unidmvol  25522  resinf1o  26517  divlogrlim  26616  dvloglem  26629  logf1o2  26631  atansssdm  26914  ppiub  27185  bday1  27824  lrrecse  27952  clwwlkn0  30117  sspval  30813  shintcli  31419  lnopco0i  32094  imaelshi  32148  nmopadjlem  32179  nmoptrii  32184  nmopcoi  32185  nmopcoadji  32191  idleop  32221  hmopidmchi  32241  hmopidmpji  32242  djussxp2  32740  xrsclat  33090  rearchi  33425  dmvlsiga  34293  sxbrsigalem0  34435  dya2iocucvr  34448  eulerpartlemgh  34542  bnj110  35020  subfacp1lem1  35381  erdszelem2  35394  dfon2lem3  35985  filnetlem2  36581  ttciunun  36713  taupi  37657  cnviun  44099  coiun1  44101  comptiunov2i  44155  cotrcltrcl  44174  cotrclrcl  44191  ssrab2f  45569  iooinlbub  45953  stirlinglem14  46537  sssalgen  46785  fvmptrabdm  47757  stgr0  48452  unilbss  49309  dfinito4  49992