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  2723  eqriv  2726  nfci  2879  abid2f  2922  abid2fOLD  2923  rgen  3046  rabeqcOLD  3657  ssriv  3950  nel0  4317  rab0  4349  ssmin  4931  intab  4942  iunab  5015  iinab  5032  sndisj  5099  disjxsn  5101  abex  5281  intidOLD  5418  fr0  5616  relssi  5750  dmi  5885  dmep  5887  onfr  6371  funopabeq  6552  isarep2  6608  opabiotafun  6941  fvopab3ig  6964  opabex  7194  caovmo  7626  trom  7851  tz7.44lem1  8373  pwfir  9266  dfsup2  9395  zfregfr  9558  dfom3  9600  dfttrcl2  9677  trcl  9681  tc2  9695  rankf  9747  rankval4  9820  uniwun  10693  dfnn2  12199  dfuzi  12625  fzodisj  13654  fzodisjsn  13658  cycsubg  19140  efger  19648  made0  27785  lrrecfr  27850  dfn0s2  28224  ajfuni  30788  funadj  31815  rabexgfGS  32428  abrexdomjm  32436  ballotth  34529  bnj1133  34979  satfv0fun  35358  fmla0xp  35370  dfon3  35880  fnsingle  35907  dfiota3  35911  hftr  36170  bj-rabtrALT  36919  ismblfin  37655  abrexdom  37724  cllem0  43555  cotrintab  43603  brtrclfv2  43716  snhesn  43775  psshepw  43777  k0004val0  44143  scottabf  44229  compab  44431  onfrALT  44539  dvcosre  45910  upwordnul  46878  upwordsing  46882  cfsetssfset  47057  alimp-surprise  49769