Theorem mpgbir 1800

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

Syntax hints:   ↔ wb 206  ∀wal 1539

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  cvjust  2728  eqriv  2731  nfci  2884  abid2f  2927  abid2fOLD  2928  rgen  3051  ssriv  3935  nel0  4304  rab0  4336  ssmin  4920  intab  4931  iunab  5005  iinab  5021  sndisj  5088  disjxsn  5090  fr0  5600  relssi  5734  dmi  5868  dmep  5870  onfr  6354  funopabeq  6526  isarep2  6580  opabiotafun  6912  fvopab3ig  6935  opabex  7164  caovmo  7593  trom  7815  tz7.44lem1  8334  pwfir  9215  dfsup2  9345  zfregfr  9511  dfom3  9554  dfttrcl2  9631  trcl  9635  tc2  9647  rankf  9704  rankval4  9777  uniwun  10649  dfnn2  12156  dfuzi  12581  fzodisj  13607  fzodisjsn  13611  cycsubg  19135  efger  19645  made0  27845  lrrecfr  27913  dfn0s2  28292  ajfuni  30883  funadj  31910  rabexgfGS  32523  abrexdomjm  32531  ballotth  34644  bnj1133  35094  satfv0fun  35514  fmla0xp  35526  dfon3  36033  fnsingle  36060  dfiota3  36064  hftr  36325  bj-rabtrALT  37075  ismblfin  37801  abrexdom  37870  cllem0  43749  cotrintab  43797  brtrclfv2  43910  snhesn  43969  psshepw  43971  k0004val0  44337  scottabf  44423  compab  44624  onfrALT  44732  dvcosre  46098  cfsetssfset  47244  alimp-surprise  49967