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  3266  rabnc  3484  ssintub  3893  tron  4418  djussxp  4812  dmiin  4913  dfco2  5170  coiun  5180  tfrlem6  6383  oacl  6527  sbthlem1  7032  peano1nnnn  7938  renfdisj  8105  1nn  9020  ioomax  10042  iccmax  10043  xnn0nnen  10548  fxnn0nninf  10550  fisumcom2  11622  fprodcom2fi  11810  bezoutlemmain  12192  dfphi2  12415  unennn  12641  znnen  12642  istopon  14357  neipsm  14498  lgsquadlem2  15427  bj-omtrans2  15711  nninfomnilem  15773  exmidsbthrlem  15779