Theorem mprgbir 2588

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2200  ∀wral 2508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1495

This theorem depends on definitions:  df-bi 117  df-ral 2513

This theorem is referenced by:  ss2rabi  3306  rabnc  3524  ssintub  3941  tron  4473  djussxp  4867  dmiin  4970  dfco2  5228  coiun  5238  tfrlem6  6462  oacl  6606  sbthlem1  7124  peano1nnnn  8039  renfdisj  8206  1nn  9121  ioomax  10144  iccmax  10145  xnn0nnen  10659  fxnn0nninf  10661  fisumcom2  11949  fprodcom2fi  12137  bezoutlemmain  12519  dfphi2  12742  unennn  12968  znnen  12969  istopon  14687  neipsm  14828  lgsquadlem2  15757  pw0ss  15883  bj-omtrans2  16320  nninfomnilem  16384  exmidsbthrlem  16390