Theorem mprgbir 2548

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2160  ∀wral 2468

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 2473

This theorem is referenced by:  ss2rabi  3252  rabnc  3470  ssintub  3877  tron  4400  djussxp  4790  dmiin  4891  dfco2  5146  coiun  5156  tfrlem6  6340  oacl  6484  sbthlem1  6985  peano1nnnn  7880  renfdisj  8046  1nn  8959  ioomax  9977  iccmax  9978  fxnn0nninf  10468  fisumcom2  11477  fprodcom2fi  11665  bezoutlemmain  12030  dfphi2  12251  unennn  12447  znnen  12448  istopon  13965  neipsm  14106  bj-omtrans2  15162  nninfomnilem  15221  exmidsbthrlem  15224