Theorem mpgbir 1802

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

Syntax hints:   ↔ wb 205  ∀wal 1540

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  cvjust  2727  eqriv  2730  nfci  2887  abid2f  2937  abid2fOLD  2938  rgen  3064  rabeqcOLD  3682  ssriv  3987  ss2abiOLD  4065  nel0  4351  rab0  4383  abfOLD  4404  ssmin  4972  intab  4983  iunab  5055  iinab  5072  sndisj  5140  disjxsn  5142  intidOLD  5459  fr0  5656  relssi  5788  dmi  5922  dmep  5924  onfr  6404  funopabeq  6585  isarep2  6640  opabiotafun  6973  fvopab3ig  6995  opabex  7222  caovmo  7644  trom  7864  tz7.44lem1  8405  pwfir  9176  dfsup2  9439  zfregfr  9600  dfom3  9642  dfttrcl2  9719  trcl  9723  tc2  9737  rankf  9789  rankval4  9862  uniwun  10735  dfnn2  12225  dfuzi  12653  fzodisj  13666  fzodisjsn  13670  cycsubg  19085  efger  19586  made0  27368  lrrecfr  27427  ajfuni  30112  funadj  31139  rabexgfGS  31739  abrexdomjm  31744  ballotth  33536  bnj1133  34000  satfv0fun  34362  fmla0xp  34374  dfon3  34864  fnsingle  34891  dfiota3  34895  hftr  35154  bj-rabtrALT  35811  ismblfin  36529  abrexdom  36598  cllem0  42317  cotrintab  42365  brtrclfv2  42478  snhesn  42537  psshepw  42539  k0004val0  42905  scottabf  42999  compab  43201  onfrALT  43310  dvcosre  44628  upwordnul  45594  upwordsing  45598  cfsetssfset  45766  alimp-surprise  47827