Theorem mprgbir 2608

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  ss2rabi  3330  rabnc  3555  ssintub  3988  tron  4529  djussxp  4927  dmiin  5030  dfco2  5290  coiun  5300  tfrlem6  6592  oacl  6738  sbthlem1  7281  peano1nnnn  8225  renfdisj  8391  1nn  9324  ioomax  10366  iccmax  10367  xnn0nnen  10894  fxnn0nninf  10896  fisumcom2  12229  fprodcom2fi  12417  bezoutlemmain  12799  dfphi2  13026  unennn  13345  znnen  13346  istopon  15256  neipsm  15397  ppiqub  16310  lgsquadlem2  16419  pw0ss  16546  clwwlkn0  16871  bj-omtrans2  17205  nninfomnilem  17284  exmidsbthrlem  17290  rirrdisj  17308