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  2066  cvjust  2729  eqriv  2732  nfci  2886  abid2f  2929  abid2fOLD  2930  rgen  3053  rabeqcOLD  3669  ssriv  3962  nel0  4329  rab0  4361  ssmin  4943  intab  4954  iunab  5027  iinab  5044  sndisj  5111  disjxsn  5113  abex  5296  intidOLD  5433  fr0  5632  relssi  5766  dmi  5901  dmep  5903  onfr  6391  funopabeq  6571  isarep2  6627  opabiotafun  6958  fvopab3ig  6981  opabex  7211  caovmo  7642  trom  7868  tz7.44lem1  8417  pwfir  9325  dfsup2  9454  zfregfr  9617  dfom3  9659  dfttrcl2  9736  trcl  9740  tc2  9754  rankf  9806  rankval4  9879  uniwun  10752  dfnn2  12251  dfuzi  12682  fzodisj  13708  fzodisjsn  13712  cycsubg  19189  efger  19697  made0  27829  lrrecfr  27893  dfn0s2  28253  ajfuni  30786  funadj  31813  rabexgfGS  32426  abrexdomjm  32434  ballotth  34516  bnj1133  34966  satfv0fun  35339  fmla0xp  35351  dfon3  35856  fnsingle  35883  dfiota3  35887  hftr  36146  bj-rabtrALT  36895  ismblfin  37631  abrexdom  37700  cllem0  43537  cotrintab  43585  brtrclfv2  43698  snhesn  43757  psshepw  43759  k0004val0  44125  scottabf  44212  compab  44414  onfrALT  44522  dvcosre  45889  upwordnul  46857  upwordsing  46861  cfsetssfset  47033  alimp-surprise  49592