Theorem mprgbir 2566

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2178  ∀wral 2486

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 1473

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

This theorem is referenced by:  ss2rabi  3283  rabnc  3501  ssintub  3917  tron  4447  djussxp  4841  dmiin  4943  dfco2  5201  coiun  5211  tfrlem6  6425  oacl  6569  sbthlem1  7085  peano1nnnn  8000  renfdisj  8167  1nn  9082  ioomax  10105  iccmax  10106  xnn0nnen  10619  fxnn0nninf  10621  fisumcom2  11864  fprodcom2fi  12052  bezoutlemmain  12434  dfphi2  12657  unennn  12883  znnen  12884  istopon  14600  neipsm  14741  lgsquadlem2  15670  pw0ss  15794  bj-omtrans2  16092  nninfomnilem  16157  exmidsbthrlem  16163