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  3654  ssriv  3947  nel0  4313  rab0  4345  ssmin  4927  intab  4938  iunab  5010  iinab  5027  sndisj  5094  disjxsn  5096  abex  5276  intidOLD  5413  fr0  5609  relssi  5741  dmi  5875  dmep  5877  onfr  6359  funopabeq  6536  isarep2  6590  opabiotafun  6923  fvopab3ig  6946  opabex  7176  caovmo  7606  trom  7831  tz7.44lem1  8350  pwfir  9242  dfsup2  9371  zfregfr  9534  dfom3  9576  dfttrcl2  9653  trcl  9657  tc2  9671  rankf  9723  rankval4  9796  uniwun  10669  dfnn2  12175  dfuzi  12601  fzodisj  13630  fzodisjsn  13634  cycsubg  19116  efger  19624  made0  27761  lrrecfr  27826  dfn0s2  28200  ajfuni  30761  funadj  31788  rabexgfGS  32401  abrexdomjm  32409  ballotth  34502  bnj1133  34952  satfv0fun  35331  fmla0xp  35343  dfon3  35853  fnsingle  35880  dfiota3  35884  hftr  36143  bj-rabtrALT  36892  ismblfin  37628  abrexdom  37697  cllem0  43528  cotrintab  43576  brtrclfv2  43689  snhesn  43748  psshepw  43750  k0004val0  44116  scottabf  44202  compab  44404  onfrALT  44512  dvcosre  45883  upwordnul  46851  upwordsing  46855  cfsetssfset  47030  alimp-surprise  49742