Theorem mprgbir 2555

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2167  ∀wral 2475

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 1463

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

This theorem is referenced by:  ss2rabi  3265  rabnc  3483  ssintub  3892  tron  4417  djussxp  4811  dmiin  4912  dfco2  5169  coiun  5179  tfrlem6  6374  oacl  6518  sbthlem1  7023  peano1nnnn  7919  renfdisj  8086  1nn  9001  ioomax  10023  iccmax  10024  xnn0nnen  10529  fxnn0nninf  10531  fisumcom2  11603  fprodcom2fi  11791  bezoutlemmain  12165  dfphi2  12388  unennn  12614  znnen  12615  istopon  14249  neipsm  14390  lgsquadlem2  15319  bj-omtrans2  15603  nninfomnilem  15662  exmidsbthrlem  15666