Theorem mpgbir 1799

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 1795	. 2 ⊢ ∀𝑥𝜓
3		mpgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥𝜓)
4	2, 3	mpbir 231	1 ⊢ 𝜑

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  sbt  2067  cvjust  2730  eqriv  2733  nfci  2887  abid2f  2930  abid2fOLD  2931  rgen  3054  rabeqcOLD  3674  ssriv  3967  nel0  4334  rab0  4366  ssmin  4948  intab  4959  iunab  5032  iinab  5049  sndisj  5116  disjxsn  5118  abex  5301  intidOLD  5438  fr0  5637  relssi  5771  dmi  5906  dmep  5908  onfr  6396  funopabeq  6577  isarep2  6633  opabiotafun  6964  fvopab3ig  6987  opabex  7217  caovmo  7649  trom  7875  tz7.44lem1  8424  pwfir  9332  dfsup2  9461  zfregfr  9624  dfom3  9666  dfttrcl2  9743  trcl  9747  tc2  9761  rankf  9813  rankval4  9886  uniwun  10759  dfnn2  12258  dfuzi  12689  fzodisj  13715  fzodisjsn  13719  cycsubg  19196  efger  19704  made0  27842  lrrecfr  27907  dfn0s2  28281  ajfuni  30845  funadj  31872  rabexgfGS  32485  abrexdomjm  32493  ballotth  34575  bnj1133  35025  satfv0fun  35398  fmla0xp  35410  dfon3  35915  fnsingle  35942  dfiota3  35946  hftr  36205  bj-rabtrALT  36954  ismblfin  37690  abrexdom  37759  cllem0  43565  cotrintab  43613  brtrclfv2  43726  snhesn  43785  psshepw  43787  k0004val0  44153  scottabf  44239  compab  44441  onfrALT  44549  dvcosre  45921  upwordnul  46889  upwordsing  46893  cfsetssfset  47065  alimp-surprise  49624