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 1537

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  2733  eqriv  2736  nfci  2891  abid2f  2940  rgen  3075  rabeqc  3623  ssriv  3926  ss2abiOLD  4002  nel0  4285  rab0  4317  abfOLD  4338  ssmin  4899  intab  4910  iunab  4982  iinab  4998  sndisj  5066  disjxsn  5068  intid  5374  fr0  5569  relssi  5699  dmi  5833  dmep  5835  onfr  6309  funopabeq  6477  isarep2  6532  opabiotafun  6858  fvopab3ig  6880  opabex  7105  caovmo  7518  trom  7730  tz7.44lem1  8245  pwfir  8968  dfsup2  9212  zfregfr  9372  dfom3  9414  dfttrcl2  9491  trcl  9495  tc2  9509  rankf  9561  rankval4  9634  uniwun  10505  dfnn2  11995  dfuzi  12420  fzodisj  13430  fzodisjsn  13434  cycsubg  18836  efger  19333  ajfuni  29230  funadj  30257  rabexgfGS  30855  abrexdomjm  30861  ballotth  32513  bnj1133  32978  satfv0fun  33342  fmla0xp  33354  made0  34066  lrrecfr  34109  dfon3  34203  fnsingle  34230  dfiota3  34234  hftr  34493  bj-rabtrALT  35128  ismblfin  35827  abrexdom  35897  cllem0  41180  cotrintab  41229  brtrclfv2  41342  snhesn  41401  psshepw  41403  k0004val0  41771  scottabf  41865  compab  42067  onfrALT  42176  dvcosre  43460  cfsetssfset  44561  alimp-surprise  46495  upwordnul  46526  upwordsing  46530