Theorem mprgbir 2552

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2164  ∀wral 2472

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 1460

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

This theorem is referenced by:  ss2rabi  3262  rabnc  3480  ssintub  3889  tron  4414  djussxp  4808  dmiin  4909  dfco2  5166  coiun  5176  tfrlem6  6371  oacl  6515  sbthlem1  7018  peano1nnnn  7914  renfdisj  8081  1nn  8995  ioomax  10017  iccmax  10018  xnn0nnen  10511  fxnn0nninf  10513  fisumcom2  11584  fprodcom2fi  11772  bezoutlemmain  12138  dfphi2  12361  unennn  12557  znnen  12558  istopon  14192  neipsm  14333  lgsquadlem2  15235  bj-omtrans2  15519  nninfomnilem  15578  exmidsbthrlem  15582