Theorem mprgbir 3060

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 3055	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓
3		mprgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
4	2, 3	mpbir 232	1 ⊢ 𝜑

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2119  ∀wral 3053

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

This theorem depends on definitions:  df-bi 208  df-ral 3054

This theorem is referenced by:  ssintub  4897  djussxp  5788  dmiin  5896  dfco2  6197  coiun  6209  tron  6334  onxpdisj  6438  epweon  7719  frrlem6  8232  frrlem7  8233  tfrlem6  8312  oawordeulem  8480  sbthlem1  9016  marypha2lem1  9339  ttrclselem1  9638  rankval4  9783  tcwf  9799  inlresf  9830  inrresf  9832  fin23lem16  10249  fin23lem29  10255  fin23lem30  10256  itunitc  10335  acncc  10354  wfgru  10731  renfdisj  11197  ioomax  13367  iccmax  13368  hashgval2  14332  fsumcom2  15728  fprodcom2  15941  dfphi2  16736  oppccatf  17686  dmcoass  18025  letsr  18551  smndex2dnrinv  18878  efgsf  19696  lssuni  20930  lpival  21318  cnsubdrglem  21394  retos  21594  psr1baslem  22171  istopon  22896  neips  23097  filssufilg  23895  xrhmeo  24932  iscmet3i  25298  ehlbase  25401  ovolge0  25467  unidmvol  25527  resinf1o  26519  divlogrlim  26618  dvloglem  26631  logf1o2  26633  atansssdm  26916  ppiub  27186  bday1  27825  lrrecse  27953  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  32741  xrsclat  33091  rearchi  33430  dmvlsiga  34322  sxbrsigalem0  34464  dya2iocucvr  34477  eulerpartlemgh  34571  bnj110  35049  subfacp1lem1  35416  erdszelem2  35429  dfon2lem3  36020  filnetlem2  36616  ttciunun  36748  taupi  37692  cnviun  44103  coiun1  44105  comptiunov2i  44159  cotrcltrcl  44178  cotrclrcl  44195  ssrab2f  45572  iooinlbub  45954  stirlinglem14  46538  sssalgen  46786  fvmptrabdm  47764  stgr0  48459  unilbss  49316  dfinito4  49999