Theorem mprgbir 2564

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2176  ∀wral 2484

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 1472

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

This theorem is referenced by:  ss2rabi  3275  rabnc  3493  ssintub  3903  tron  4429  djussxp  4823  dmiin  4924  dfco2  5182  coiun  5192  tfrlem6  6402  oacl  6546  sbthlem1  7059  peano1nnnn  7965  renfdisj  8132  1nn  9047  ioomax  10070  iccmax  10071  xnn0nnen  10582  fxnn0nninf  10584  fisumcom2  11749  fprodcom2fi  11937  bezoutlemmain  12319  dfphi2  12542  unennn  12768  znnen  12769  istopon  14485  neipsm  14626  lgsquadlem2  15555  bj-omtrans2  15893  nninfomnilem  15955  exmidsbthrlem  15961