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  6591  oacl  6737  sbthlem1  7279  peano1nnnn  8225  renfdisj  8391  1nn  9324  ioomax  10367  iccmax  10368  xnn0nnen  10895  fxnn0nninf  10897  fisumcom2  12230  fprodcom2fi  12418  bezoutlemmain  12800  dfphi2  13027  unennn  13346  znnen  13347  istopon  15239  neipsm  15380  ppiqub  16293  lgsquadlem2  16402  pw0ss  16529  clwwlkn0  16854  bj-omtrans2  17188  nninfomnilem  17267  exmidsbthrlem  17273  rirrdisj  17291