Theorem mprgbir 2524

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

Syntax hints:   → wi 4   ↔ wb 104   ∈ wcel 2136  ∀wral 2444

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

This theorem depends on definitions:  df-bi 116  df-ral 2449

This theorem is referenced by:  ss2rabi  3224  rabnc  3441  ssintub  3842  tron  4360  djussxp  4749  dmiin  4850  dfco2  5103  coiun  5113  tfrlem6  6284  oacl  6428  sbthlem1  6922  peano1nnnn  7793  renfdisj  7958  1nn  8868  ioomax  9884  iccmax  9885  fxnn0nninf  10373  fisumcom2  11379  fprodcom2fi  11567  bezoutlemmain  11931  dfphi2  12152  unennn  12330  znnen  12331  istopon  12651  neipsm  12794  bj-omtrans2  13839  nninfomnilem  13898  exmidsbthrlem  13901