Theorem mprgbir 2608

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2209  ∀wral 2528

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 1502

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

This theorem is referenced by:  ss2rabi  3330  rabnc  3555  ssintub  3983  tron  4522  djussxp  4920  dmiin  5023  dfco2  5282  coiun  5292  tfrlem6  6577  oacl  6723  sbthlem1  7264  peano1nnnn  8209  renfdisj  8375  1nn  9294  ioomax  10329  iccmax  10330  xnn0nnen  10852  fxnn0nninf  10854  fisumcom2  12183  fprodcom2fi  12371  bezoutlemmain  12753  dfphi2  12976  unennn  13266  znnen  13267  istopon  15037  neipsm  15178  lgsquadlem2  16111  pw0ss  16238  clwwlkn0  16563  bj-omtrans2  16897  nninfomnilem  16966  exmidsbthrlem  16972