Theorem mpgbir 1801

Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)

Hypotheses

Ref	Expression
mpgbir.1	⊢ (𝜑 ↔ ∀𝑥𝜓)
mpgbir.2	⊢ 𝜓

Assertion

Ref	Expression
mpgbir	⊢ 𝜑

Proof of Theorem mpgbir

Step	Hyp	Ref	Expression
1		mpgbir.2	. . 3 ⊢ 𝜓
2	1	ax-gen 1797	. 2 ⊢ ∀𝑥𝜓
3		mpgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥𝜓)
4	2, 3	mpbir 231	1 ⊢ 𝜑

Syntax hints:   ↔ wb 206  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  cvjust  2730  eqriv  2733  nfci  2886  abid2f  2929  abid2fOLD  2930  rgen  3053  ssriv  3925  nel0  4294  rab0  4326  ssmin  4909  intab  4920  sndisj  5077  disjxsn  5079  fr0  5609  relssi  5743  dmi  5876  dmep  5878  onfr  6362  funopabeq  6534  isarep2  6588  opabiotafun  6920  fvopab3ig  6943  opabex  7175  caovmo  7604  trom  7826  tz7.44lem1  8344  pwfir  9227  dfsup2  9357  zfregfr  9525  dfom3  9568  dfttrcl2  9645  trcl  9649  tc2  9661  rankf  9718  rankval4  9791  uniwun  10663  dfnn2  12187  dfuzi  12620  fzodisj  13648  fzodisjsn  13652  cycsubg  19183  efger  19693  made0  27855  lrrecfr  27935  dfn0s2  28324  ajfuni  30930  funadj  31957  rabexgfGS  32569  abrexdomjm  32577  ballotth  34682  bnj1133  35131  satfv0fun  35553  fmla0xp  35565  dfon3  36072  fnsingle  36099  dfiota3  36103  hftr  36364  tz9.1tco  36665  dfttc3gw  36705  bj-rabtrALT  37238  ismblfin  37982  abrexdom  38051  cllem0  43993  cotrintab  44041  brtrclfv2  44154  snhesn  44213  psshepw  44215  k0004val0  44581  scottabf  44667  compab  44868  onfrALT  44976  dvcosre  46340  cfsetssfset  47504  alimp-surprise  50255