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  2731  eqriv  2734  nfci  2887  abid2f  2930  abid2fOLD  2931  rgen  3054  ssriv  3939  nel0  4308  rab0  4340  ssmin  4924  intab  4935  iunab  5009  iinab  5025  sndisj  5092  disjxsn  5094  fr0  5610  relssi  5744  dmi  5878  dmep  5880  onfr  6364  funopabeq  6536  isarep2  6590  opabiotafun  6922  fvopab3ig  6945  opabex  7176  caovmo  7605  trom  7827  tz7.44lem1  8346  pwfir  9229  dfsup2  9359  zfregfr  9525  dfom3  9568  dfttrcl2  9645  trcl  9649  tc2  9661  rankf  9718  rankval4  9791  uniwun  10663  dfnn2  12170  dfuzi  12595  fzodisj  13621  fzodisjsn  13625  cycsubg  19149  efger  19659  made0  27871  lrrecfr  27951  dfn0s2  28340  ajfuni  30947  funadj  31974  rabexgfGS  32586  abrexdomjm  32594  ballotth  34716  bnj1133  35165  satfv0fun  35587  fmla0xp  35599  dfon3  36106  fnsingle  36133  dfiota3  36137  hftr  36398  bj-rabtrALT  37179  ismblfin  37912  abrexdom  37981  cllem0  43922  cotrintab  43970  brtrclfv2  44083  snhesn  44142  psshepw  44144  k0004val0  44510  scottabf  44596  compab  44797  onfrALT  44905  dvcosre  46270  cfsetssfset  47416  alimp-surprise  50139