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  4527  djussxp  4925  dmiin  5028  dfco2  5287  coiun  5297  tfrlem6  6587  oacl  6733  sbthlem1  7274  peano1nnnn  8219  renfdisj  8385  1nn  9317  ioomax  10360  iccmax  10361  xnn0nnen  10887  fxnn0nninf  10889  fisumcom2  12221  fprodcom2fi  12409  bezoutlemmain  12791  dfphi2  13018  unennn  13337  znnen  13338  istopon  15163  neipsm  15304  ppiqub  16194  lgsquadlem2  16295  pw0ss  16422  clwwlkn0  16747  bj-omtrans2  17081  nninfomnilem  17159  exmidsbthrlem  17165