Theorem mpgbir 1797

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

Syntax hints:   ↔ wb 206  ∀wal 1535

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  cvjust  2734  eqriv  2737  nfci  2896  abid2f  2942  abid2fOLD  2943  rgen  3069  rabeqcOLD  3706  ssriv  4012  nel0  4377  rab0  4409  ssmin  4991  intab  5002  iunab  5074  iinab  5091  sndisj  5158  disjxsn  5160  abex  5344  intidOLD  5478  fr0  5678  relssi  5811  dmi  5946  dmep  5948  onfr  6434  funopabeq  6614  isarep2  6669  opabiotafun  7002  fvopab3ig  7025  opabex  7257  caovmo  7687  trom  7912  tz7.44lem1  8461  pwfir  9383  dfsup2  9513  zfregfr  9674  dfom3  9716  dfttrcl2  9793  trcl  9797  tc2  9811  rankf  9863  rankval4  9936  uniwun  10809  dfnn2  12306  dfuzi  12734  fzodisj  13750  fzodisjsn  13754  cycsubg  19248  efger  19760  made0  27930  lrrecfr  27994  dfn0s2  28354  ajfuni  30891  funadj  31918  rabexgfGS  32527  abrexdomjm  32535  ballotth  34502  bnj1133  34965  satfv0fun  35339  fmla0xp  35351  dfon3  35856  fnsingle  35883  dfiota3  35887  hftr  36146  bj-rabtrALT  36897  ismblfin  37621  abrexdom  37690  cllem0  43528  cotrintab  43576  brtrclfv2  43689  snhesn  43748  psshepw  43750  k0004val0  44116  scottabf  44209  compab  44411  onfrALT  44520  dvcosre  45833  upwordnul  46799  upwordsing  46803  cfsetssfset  46971  alimp-surprise  48874